kkytola

Results 6 comments of kkytola

feat(measure_theory/measure/finite_measure_weak_convergence): Add portmanteau implications concerning open and closed sets.

bors r+

feat(MeasureTheory/Integral/linearRieszMarkovKakutani) prove that the Riesz content is indeed a content

> I tried to do the `NNReal` version myself, and I found that the proof of additivity `rieszContentAux_eq_add` is painful: one should take, using Urysohn's lemma, a function `g` which...

feat(MeasureTheory/Integral/linearRieszMarkovKakutani) prove that the Riesz content is indeed a content

I made #12559 which enables subtraction for nonnegative bounded continuous functions. If the model (new type class and otherwise minimal changes) is considered reasonable, I will do a similar PR...

feat(MeasureTheory/Integral/linearRieszMarkovKakutani) prove that the Riesz content is indeed a content

Now that #12790 and #12559 are in Mathlib and one can subtract and multiply bounded continuous functions, showing that the `rieszContentAux` gives rise to an actual content (`rieszContent` below) is...

feat(MeasureTheory/Integral/linearRieszMarkovKakutani) prove that the Riesz content is indeed a content

> Nice! I am not sure how to proceed: I wrote myself the characterization of the measure for linear `Λ`, although it needs much refactoring (one remaining `sorry` is just...

feat(MeasureTheory/Integral/linearRieszMarkovKakutani) prove that the Riesz content is indeed a content

> Nice! I am not sure how to proceed: I wrote myself the characterization of the measure for linear `Λ`, although it needs much refactoring (one remaining `sorry` is just...