OAI/Analysis/Brenier/DensityCDF.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Problem358.PositiveIntervalDensity line 11

   Source documentation

   A positive continuous density on an open bounded interval. Endpoint values are irrelevant.

   structure PositiveIntervalDensity where
   …

2. def OAI.Problem358.PositiveIntervalDensity.cdf line 26

   Source documentation

   The cumulative integral starting at the lower endpoint.

   def cdf (x : ℝ) : ℝ := ∫ t in D.lower..x, D.density t

3. lemma OAI.Problem358.PositiveIntervalDensity.cdf_lower line 28
4. lemma OAI.Problem358.PositiveIntervalDensity.cdf_upper line 29
5. lemma OAI.Problem358.PositiveIntervalDensity.cdf_continuousOn line 31
6. lemma OAI.Problem358.PositiveIntervalDensity.cdf_hasDerivAt line 36
7. lemma OAI.Problem358.PositiveIntervalDensity.cdf_strictMonoOn line 46
8. lemma OAI.Problem358.PositiveIntervalDensity.cdf_image line 53
9. lemma OAI.Problem358.PositiveIntervalDensity.existsUnique_cdf_eq line 58
10. def OAI.Problem358.PositiveIntervalDensity.cdfOrderIso line 79

    Source documentation

    Cumulative integration is an order isomorphism between the two compact intervals.

    def cdfOrderIso : Icc D.lower D.upper ≃o Icc (0 : ℝ) 1 :=
    …

11. def OAI.Problem358.PositiveIntervalDensity.quantile line 84

    Source documentation

    The inverse cumulative map, including its continuous endpoint extension.

    def quantile (s : Icc (0 : ℝ) 1) : ℝ := (D.cdfOrderIso.symm s).1

12. lemma OAI.Problem358.PositiveIntervalDensity.quantile_mem line 86
13. lemma OAI.Problem358.PositiveIntervalDensity.quantile_continuous line 89
14. lemma OAI.Problem358.PositiveIntervalDensity.cdf_quantile line 92
15. lemma OAI.Problem358.PositiveIntervalDensity.quantile_mem_interior line 96
16. def OAI.Problem358.PositiveIntervalDensity.quantileReal line 111

    Source documentation

    A globally continuous extension of the quantile, constant outside the unit interval.

    def quantileReal (s : ℝ) : ℝ := D.quantile (Set.projIcc 0 1 (by norm_num) s)

17. lemma OAI.Problem358.PositiveIntervalDensity.quantileReal_continuous line 113
18. lemma OAI.Problem358.PositiveIntervalDensity.quantileReal_eq line 116
19. lemma OAI.Problem358.PositiveIntervalDensity.cdf_quantileReal line 120
20. lemma OAI.Problem358.PositiveIntervalDensity.quantileReal_mem_interior line 125
21. lemma OAI.Problem358.PositiveIntervalDensity.quantileReal_hasDerivAt line 131

    Source documentation

    The one-dimensional inverse-density derivative used in the triangular coupling.

    lemma quantileReal_hasDerivAt {s : ℝ} (hs : s ∈ Ioo (0 : ℝ) 1) :
        HasDerivAt D.quantileReal (D.density (D.quantileReal s))⁻¹ s := by
    …

22. lemma OAI.Problem358.PositiveIntervalDensity.quantileReal_deriv_pos line 139
23. lemma OAI.Problem358.PositiveIntervalDensity.cdf_image_Ioo line 144
24. lemma OAI.Problem358.PositiveIntervalDensity.quantileReal_mem line 148
25. lemma OAI.Problem358.PositiveIntervalDensity.quantileReal_cdf line 151
26. def OAI.Problem358.PositiveIntervalDensity.densityMeasure line 160

    Source documentation

    The probability distribution with the given density, restricted to its open interval.

    def densityMeasure : Measure ℝ :=
    …

27. lemma OAI.Problem358.PositiveIntervalDensity.densityMeasure_ae_mem line 163
28. lemma OAI.Problem358.PositiveIntervalDensity.cdf_aemeasurable line 167
29. lemma OAI.Problem358.PositiveIntervalDensity.map_cdf_densityMeasure line 172

    Source documentation

    The change-of-variables theorem sends the positive density to the unit uniform law.

    lemma map_cdf_densityMeasure :
        Measure.map D.cdf D.densityMeasure = volume.restrict (Ioo (0 : ℝ) 1) := by
    …

30. lemma OAI.Problem358.PositiveIntervalDensity.map_quantileReal_uniform line 188

    Source documentation

    The quantile constructed above really has the prescribed density law.

    lemma map_quantileReal_uniform :
        Measure.map D.quantileReal (volume.restrict (Ioo (0 : ℝ) 1)) = D.densityMeasure := by
    …

31. instance OAI.Problem358.PositiveIntervalDensity.densityMeasure_isProbabilityMeasure line 200
32. lemma OAI.Problem358.PositiveIntervalDensity.lintegral_quantileReal line 207
33. lemma OAI.Problem358.PositiveIntervalDensity.integral_quantileReal line 212
34. lemma OAI.Problem358.PositiveIntervalDensity.quantileReal_lt_iff line 219

    Source documentation

    Inverse thresholds reduce parameter measurability to cumulative-integral evaluations.

    lemma quantileReal_lt_iff {s r : ℝ} (hs : s ∈ Ioo (0 : ℝ) 1) :
        D.quantileReal s < r ↔ D.lower < r ∧ (D.upper ≤ r ∨ s < D.cdf r) := by
    …

35. theorem OAI.Problem358.PositiveIntervalDensity.measurable_quantileReal_family line 242

    Source documentation

    Measurable parameters give measurable interior quantiles. The density structures themselves need no chosen measurable-space architecture: only endpoint and cumulative evaluations matter.

    theorem measurable_quantileReal_family {Ω : Type*} [MeasurableSpace Ω]
        (D : Ω → PositiveIntervalDensity)
        (hlower : Measurable fun ω => (D ω).lower)
        (hupper : Measurable fun ω => (D ω).upper)
        (hcdf : ∀ r : ℝ, Measurable fun ω => (D ω).cdf r)
        {s : Ω → ℝ} (hs : Measurable s) (hsrange : ∀ ω, s ω ∈ Ioo (0 : ℝ) 1) :
        Measurable (fun ω => (D ω).quantileReal (s ω)) := by
    …

    Mentions: OAI.Problem358.PositiveIntervalDensity, OAI.Problem358.PositiveIntervalDensity.cdf, OAI.Problem358.PositiveIntervalDensity.quantileReal

36. theorem OAI.Problem358.PositiveIntervalDensity.measurable_joint_quantileReal line 261

    Source documentation

    Joint Borel measurability of a family of quantiles on parameter × open unit interval.

    theorem measurable_joint_quantileReal {Ω : Type*} [MeasurableSpace Ω]
        (D : Ω → PositiveIntervalDensity)
        (hlower : Measurable fun ω => (D ω).lower)
        (hupper : Measurable fun ω => (D ω).upper)
        (hcdf : ∀ r : ℝ, Measurable fun ω => (D ω).cdf r) :
        Measurable (fun z : Ω × Ioo (0 : ℝ) 1 => (D z.1).quantileReal z.2) := by
    …

    Mentions: OAI.Problem358.PositiveIntervalDensity, OAI.Problem358.PositiveIntervalDensity.cdf, OAI.Problem358.PositiveIntervalDensity.quantileReal

37. lemma OAI.Problem358.PositiveIntervalDensity.measurable_intervalIntegral_family line 274

    Source documentation

    Parameter integrals over measurable moving real intervals are measurable.

    lemma measurable_intervalIntegral_family {Ω : Type*} [MeasurableSpace Ω]
        {f : Ω × ℝ → ℝ} (hf : Measurable f) {a b : Ω → ℝ}
        (ha : Measurable a) (hb : Measurable b) :
        Measurable (fun ω => ∫ t in a ω..b ω, f (ω, t)) := by
    …

38. theorem OAI.Problem358.PositiveIntervalDensity.measurable_joint_quantileReal_of_density line 296

    Source documentation

    Jointly measurable density data give jointly measurable quantiles, as required in each recursive coordinate of a triangular inverse-CDF construction.

    theorem measurable_joint_quantileReal_of_density {Ω : Type*} [MeasurableSpace Ω]
        (D : Ω → PositiveIntervalDensity)
        (hlower : Measurable fun ω => (D ω).lower)
        (hupper : Measurable fun ω => (D ω).upper)
        (hdensity : Measurable fun z : Ω × ℝ => (D z.1).density z.2) :
        Measurable (fun z : Ω × Ioo (0 : ℝ) 1 => (D z.1).quantileReal z.2) := by
    …

    Mentions: OAI.Problem358.PositiveIntervalDensity, OAI.Problem358.PositiveIntervalDensity.quantileReal

39. lemma OAI.Problem358.PositiveIntervalDensity.quantileReal_of_nonpos line 306
40. lemma OAI.Problem358.PositiveIntervalDensity.quantileReal_of_one_le line 316
41. theorem OAI.Problem358.PositiveIntervalDensity.measurable_quantileReal_family_global line 327

    Source documentation

    The continuous extensions are jointly measurable even for parameters outside (0,1).

    theorem measurable_quantileReal_family_global {Ω : Type*} [MeasurableSpace Ω]
        (D : Ω → PositiveIntervalDensity)
        (hlower : Measurable fun ω => (D ω).lower)
        (hupper : Measurable fun ω => (D ω).upper)
        (hcdf : ∀ r : ℝ, Measurable fun ω => (D ω).cdf r)
        {s : Ω → ℝ} (hs : Measurable s) :
        Measurable (fun ω => (D ω).quantileReal (s ω)) := by
    …

    Mentions: OAI.Problem358.PositiveIntervalDensity, OAI.Problem358.PositiveIntervalDensity.cdf, OAI.Problem358.PositiveIntervalDensity.quantileReal

42. theorem OAI.Problem358.PositiveIntervalDensity.measurable_joint_quantileReal_global line 360
43. theorem OAI.Problem358.PositiveIntervalDensity.lintegral_joint_quantileReal line 373

    Source documentation

    One recursive sampling step has precisely the prescribed conditional density law.

    theorem lintegral_joint_quantileReal {Ω : Type*} [MeasurableSpace Ω]
        (μ : Measure Ω) (D : Ω → PositiveIntervalDensity)
        (hlower : Measurable fun ω => (D ω).lower)
        (hupper : Measurable fun ω => (D ω).upper)
        (hdensity : Measurable fun z : Ω × ℝ => (D z.1).density z.2)
        (f : Ω × ℝ → ℝ≥0∞) (hf : Measurable f) :
        (∫⁻ z, f (z.1, (D z.1).quantileReal z.2)
          ∂μ.prod (volume.restrict (Ioo (0 : ℝ) 1))) =
            ∫⁻ ω, ∫⁻ x, f (ω, x) ∂(D ω).densityMeasure ∂μ := by
    …

    Mentions: OAI.Problem358.PositiveIntervalDensity, OAI.Problem358.PositiveIntervalDensity.quantileReal, OAI.Problem358.PositiveIntervalDensity.densityMeasure

44. lemma OAI.Problem358.PositiveIntervalDensity.quantileReal_strictMonoOn line 391
45. theorem OAI.Problem358.PositiveIntervalDensity.exists_measurable_quantile_extension line 403

    Source documentation

    Conditional densities only need to exist on the measurable set of valid prefixes. Their quantiles extend to a globally measurable map without imposing any density law at the invalid prefixes. The extension agrees at every real argument on valid fibers.

    theorem exists_measurable_quantile_extension {Ω : Type*} [MeasurableSpace Ω]
        (S : Set Ω) (hS : MeasurableSet S) (D : S → PositiveIntervalDensity)
        (hlower : Measurable fun ω => (D ω).lower)
        (hupper : Measurable fun ω => (D ω).upper)
        (hdensity : Measurable fun z : S × ℝ => (D z.1).density z.2) :
        ∃ Q : Ω × ℝ → ℝ, Measurable Q ∧
          (∀ ω : S, ∀ s : ℝ, Q (ω, s) = (D ω).quantileReal s) ∧
          (∀ ω : S, Measure.map (fun s => Q (ω, s))
            (volume.restrict (Ioo (0 : ℝ) 1)) = (D ω).densityMeasure) ∧
          (∀ ω : S, ∀ s ∈ Ioo (0 : ℝ) 1,
            HasDerivAt (fun t => Q (ω, t)) ((D ω).density (Q (ω, s)))⁻¹ s) ∧
          (∀ ω : S, StrictMonoOn (fun s => Q (ω, s)) (Icc (0 : ℝ) 1)) := by
    …

    Mentions: OAI.Problem358.PositiveIntervalDensity, OAI.Problem358.PositiveIntervalDensity.quantileReal, OAI.Problem358.PositiveIntervalDensity.densityMeasure