[GOAL]
μ : Measure ℝ
inst✝ : IsProbabilityMeasure μ
x : ℝ
⊢ ENNReal.ofReal (↑(cdf μ) x) = ↑↑μ (Iic x)
[PROOFSTEP]
have h := lintegral_condCdf ((Measure.dirac Unit.unit).prod μ) x
[GOAL]
μ : Measure ℝ
inst✝ : IsProbabilityMeasure μ
x : ℝ
h :
  ∫⁻ (a : Unit),
      ENNReal.ofReal
        (↑(condCdf (Measure.prod (Measure.dirac ()) μ) a) x) ∂Measure.fst (Measure.prod (Measure.dirac ()) μ) =
    ↑↑(Measure.prod (Measure.dirac ()) μ) (univ ×ˢ Iic x)
⊢ ENNReal.ofReal (↑(cdf μ) x) = ↑↑μ (Iic x)
[PROOFSTEP]
simpa only [MeasureTheory.Measure.fst_prod, Measure.prod_prod, measure_univ, one_mul, lintegral_dirac] using h
[GOAL]
μ : Measure ℝ
inst✝ : IsProbabilityMeasure μ
x : ℝ
⊢ ↑(cdf μ) x = ENNReal.toReal (↑↑μ (Iic x))
[PROOFSTEP]
rw [← ofReal_cdf μ x, ENNReal.toReal_ofReal (cdf_nonneg μ x)]
[GOAL]
μ : Measure ℝ
⊢ IsProbabilityMeasure (StieltjesFunction.measure (cdf μ))
[PROOFSTEP]
constructor
[GOAL]
case measure_univ
μ : Measure ℝ
⊢ ↑↑(StieltjesFunction.measure (cdf μ)) univ = 1
[PROOFSTEP]
simp only [StieltjesFunction.measure_univ _ (tendsto_cdf_atBot μ) (tendsto_cdf_atTop μ), sub_zero, ENNReal.ofReal_one]
[GOAL]
μ : Measure ℝ
inst✝ : IsProbabilityMeasure μ
⊢ StieltjesFunction.measure (cdf μ) = μ
[PROOFSTEP]
refine Measure.ext_of_Iic (cdf μ).measure μ (fun a ↦ ?_)
[GOAL]
μ : Measure ℝ
inst✝ : IsProbabilityMeasure μ
a : ℝ
⊢ ↑↑(StieltjesFunction.measure (cdf μ)) (Iic a) = ↑↑μ (Iic a)
[PROOFSTEP]
rw [StieltjesFunction.measure_Iic _ (tendsto_cdf_atBot μ), sub_zero, ofReal_cdf]
[GOAL]
f : StieltjesFunction
hf0 : Tendsto (↑f) atBot (𝓝 0)
hf1 : Tendsto (↑f) atTop (𝓝 1)
⊢ cdf (StieltjesFunction.measure f) = f
[PROOFSTEP]
refine (cdf f.measure).eq_of_measure_of_tendsto_atBot f ?_ (tendsto_cdf_atBot _) hf0
[GOAL]
f : StieltjesFunction
hf0 : Tendsto (↑f) atBot (𝓝 0)
hf1 : Tendsto (↑f) atTop (𝓝 1)
⊢ StieltjesFunction.measure (cdf (StieltjesFunction.measure f)) = StieltjesFunction.measure f
[PROOFSTEP]
have h_prob : IsProbabilityMeasure f.measure := ⟨by rw [f.measure_univ hf0 hf1, sub_zero, ENNReal.ofReal_one]⟩
[GOAL]
f : StieltjesFunction
hf0 : Tendsto (↑f) atBot (𝓝 0)
hf1 : Tendsto (↑f) atTop (𝓝 1)
⊢ ↑↑(StieltjesFunction.measure f) univ = 1
[PROOFSTEP]
rw [f.measure_univ hf0 hf1, sub_zero, ENNReal.ofReal_one]
[GOAL]
f : StieltjesFunction
hf0 : Tendsto (↑f) atBot (𝓝 0)
hf1 : Tendsto (↑f) atTop (𝓝 1)
h_prob : IsProbabilityMeasure (StieltjesFunction.measure f)
⊢ StieltjesFunction.measure (cdf (StieltjesFunction.measure f)) = StieltjesFunction.measure f
[PROOFSTEP]
exact measure_cdf f.measure
[GOAL]
μ ν : Measure ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
h : cdf μ = cdf ν
⊢ μ = ν
[PROOFSTEP]
rw [← measure_cdf μ, ← measure_cdf ν, h]
[GOAL]
μ ν : Measure ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
h : μ = ν
⊢ cdf μ = cdf ν
[PROOFSTEP]
rw [h]
