Radon Nikodym Fun

Stream: new members

[Dominic Steinitz]

I was surprised I couldn't use Radon Nikodym directly and had to do coercions. Measures are positive? And surely one can integrate non-negative functions? I guess there is something I don't understand.

import Mathlib

open MeasureTheory ProbabilityTheory NNReal Real Filter Finset Asymptotics
open Set Filter TopologicalSpace
open Topology Filter Cardinal MeasureSpace  MeasureTheory.Measure
open BoundedContinuousFunction BoxIntegral PMF
open ENNReal ProbabilityMeasure ClosedIicTopology

example (μ : Measure ℝ) (x : ℝ) (h : μ ≪ volume) :
  μ (Iic x) = ∫ t in Iic x, (rnDeriv μ volume) t ∂volume := sorry

example (μ : Measure ℝ) (x : ℝ) (h : μ ≪ volume) :
 ENNReal.toReal (μ (Iic x)) = ∫ t in Iic x, (λ x => ENNReal.toReal ((rnDeriv μ volume) x)) t ∂volume := sorry

[Kexing Ying]

You should use lintegral to integrate ENNReal valued functions:

example (μ : Measure ℝ) [SigmaFinite μ] (x : ℝ) (h : μ ≪ volume) :
    μ (Iic x) = ∫⁻ t in Iic x, (∂μ/∂ℙ) t := by
  conv_lhs => rw [← withDensity_rnDeriv_eq μ volume h]
  simp