BorelTransport.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.Transport.exists_cdf_eq_of_continuous line 13
Source documentation
Every probability level strictly between zero and one is achieved by a continuous CDF.
```
theorem exists_cdf_eq_of_continuous (μ : Measure ℝ)
    (hc : Continuous (cdf μ)) {u : ℝ} (hu0 : 0 < u) (hu1 : u < 1) :
    ∃ x : ℝ, cdf μ x = u := by
…
```

theorem OAI.Problem356.Transport.measureReal_cdf_sublevel line 22

Source documentation

The probability integral transform, expressed on CDF sublevel sets.

theorem measureReal_cdf_sublevel (μ : Measure ℝ) [IsProbabilityMeasure μ]
    (hc : Continuous (cdf μ)) {u : ℝ} (hu0 : 0 ≤ u) (hu1 : u ≤ 1) :
    μ.real {x : ℝ | cdf μ x ≤ u} = u := by
…

theorem OAI.Problem356.Transport.map_cdf_unitInterval line 57

Source documentation

A continuous CDF sends its law to uniform probability on the unit interval.

theorem map_cdf_unitInterval (μ : Measure ℝ) [IsProbabilityMeasure μ]
    (hc : Continuous (cdf μ)) :
    μ.map (fun x : ℝ => (⟨cdf μ x, cdf_nonneg μ x, cdf_le_one μ x⟩ : I)) = volume := by
…