OAI/Analysis/Brenier/Quantiles.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem358.unique_monotone_inverse_lt_iff line 16

   Source documentation

   Comparison with the unique inverse point of a monotone real function.

   lemma unique_monotone_inverse_lt_iff {F : ℝ → ℝ} (hF : Monotone F)
       {t x : ℝ} (hx : F x = t) (huniq : ∀ y, F y = t → y = x) (q : ℝ) :
       x < q ↔ t < F q := by
   …

2. theorem OAI.Problem358.exists_measurable_monotone_inverse line 36

   Source documentation

   Parameter-dependent monotone inverses are measurable whenever their CDF sections and selected levels are measurable. Unique fibers remove any need for a measurable-choice theorem.

   theorem exists_measurable_monotone_inverse
       {A : Type*} [MeasurableSpace A] (F : A → ℝ → ℝ) (t : A → ℝ)
       (hmono : ∀ a, Monotone (F a))
       (hsection : ∀ q : ℝ, Measurable (fun a => F a q))
       (ht : Measurable t) (hex : ∀ a, ∃! x : ℝ, F a x = t a) :
       ∃ Q : A → ℝ, Measurable Q ∧ ∀ a, F a (Q a) = t a := by
   …

3. lemma OAI.Problem358.inverse_points_strictMono line 55

   Source documentation

   Inverse points of a monotone function are necessarily ordered with their levels, even if the original function has flat regions away from those fibers.

   lemma inverse_points_strictMono {F : ℝ → ℝ} (hF : Monotone F)
       {S : Set ℝ} {Q : S → ℝ} (hQ : ∀ t, F (Q t) = (t : ℝ)) :
       StrictMono Q := by
   …

4. lemma OAI.Problem358.exists_unique_monotone_inverse_of_interval line 67

   Source documentation

   A continuous strictly increasing interval reaches each intermediate level at a unique point, provided the ambient extension remains monotone.

   lemma exists_unique_monotone_inverse_of_interval {F : ℝ → ℝ} {a b t : ℝ}
       (hab : a ≤ b) (hcont : ContinuousOn F (Icc a b)) (hmono : Monotone F)
       (hstrict : StrictMonoOn F (Icc a b)) (ht : t ∈ Ioo (F a) (F b)) :
       ∃! x : ℝ, F x = t := by
   …

5. lemma OAI.Problem358.continuousAt_monotone_inverse line 89

   Source documentation

   A local inverse of a monotone real function is continuous at every level whose fiber is a singleton. No differentiability or strict global monotonicity is required.

   lemma continuousAt_monotone_inverse {F Q : ℝ → ℝ} {t : ℝ}
       (hmono : Monotone F) (hlocal : ∀ᶠ s in 𝓝 t, F (Q s) = s)
       (huniq : ∀ x, F x = t → x = Q t) : ContinuousAt Q t := by
   …

6. lemma OAI.Problem358.hasDerivAt_monotone_inverse line 115

   Source documentation

   The reciprocal-density derivative formula for a local monotone inverse.

   lemma hasDerivAt_monotone_inverse {F Q : ℝ → ℝ} {t c : ℝ}
       (hmono : Monotone F) (hlocal : ∀ᶠ s in 𝓝 t, F (Q s) = s)
       (huniq : ∀ x, F x = t → x = Q t)
       (hderiv : HasDerivAt F c (Q t)) (hc : c ≠ 0) :
       HasDerivAt Q c⁻¹ t := by
   …

7. lemma OAI.Problem358.unique_monotone_inverse_le_iff line 123
8. lemma OAI.Problem358.volume_Iic_inter_unitInterval line 136
9. theorem OAI.Problem358.map_inverse_cdf_eq line 156

   Source documentation

   A measurable inverse of a probability CDF transports unit-interval Lebesgue measure to the probability law. This is the one-dimensional law identity used in triangular quantile constructions.

   theorem map_inverse_cdf_eq (μ : Measure ℝ) [IsProbabilityMeasure μ]
       {Q : ℝ → ℝ} (hQ : Measurable Q)
       (hsolve : ∀ t ∈ Ioo (0 : ℝ) 1, ProbabilityTheory.cdf μ (Q t) = t)
       (huniq : ∀ t ∈ Ioo (0 : ℝ) 1, ∀ x,
         ProbabilityTheory.cdf μ x = t → x = Q t) :
       Measure.map Q (volume.restrict (Ioo (0 : ℝ) 1)) = μ := by
   …

10. theorem OAI.Problem358.exists_measurable_cdf_transport line 185

    Source documentation

    A probability law with unique inverse CDF points at every level in (0,1) has a measurable quantile transport, continuous at every such level.

    theorem exists_measurable_cdf_transport (μ : Measure ℝ) [IsProbabilityMeasure μ]
        (hex : ∀ t ∈ Ioo (0 : ℝ) 1, ∃! x : ℝ, ProbabilityTheory.cdf μ x = t) :
        ∃ Q : ℝ → ℝ, Measurable Q ∧
          Measure.map Q (volume.restrict (Ioo (0 : ℝ) 1)) = μ ∧
          (∀ t ∈ Ioo (0 : ℝ) 1, ProbabilityTheory.cdf μ (Q t) = t) ∧
          ∀ t ∈ Ioo (0 : ℝ) 1, ContinuousAt Q t := by
    …

11. theorem OAI.Problem358.exists_measurable_cdf_family_transport line 217

    Source documentation

    Jointly measurable quantiles for a family of one-dimensional probability laws. Only measurability of each CDF section is needed in the parameter.

    theorem exists_measurable_cdf_family_transport
        {A : Type*} [MeasurableSpace A] (κ : A → Measure ℝ)
        [∀ a, IsProbabilityMeasure (κ a)]
        (hsection : ∀ q : ℝ, Measurable (fun a => ProbabilityTheory.cdf (κ a) q))
        (hex : ∀ a t, t ∈ Ioo (0 : ℝ) 1 → ∃! x : ℝ, ProbabilityTheory.cdf (κ a) x = t) :
        ∃ Q : A × ℝ → ℝ, Measurable Q ∧
          (∀ a, Measure.map (fun t => Q (a, t)) (volume.restrict (Ioo (0 : ℝ) 1)) = κ a) ∧
          (∀ a t, t ∈ Ioo (0 : ℝ) 1 → ProbabilityTheory.cdf (κ a) (Q (a, t)) = t) ∧
          ∀ a t, t ∈ Ioo (0 : ℝ) 1 → ContinuousAt (fun s => Q (a, s)) t := by
    …

12. lemma OAI.Problem358.measurable_cdf_kernel_section line 260

    Source documentation

    CDF sections of a real-valued Markov kernel are measurable.

    lemma measurable_cdf_kernel_section {A : Type*} [MeasurableSpace A]
        (κ : ProbabilityTheory.Kernel A ℝ) [ProbabilityTheory.IsMarkovKernel κ] (q : ℝ) :
        Measurable (fun a => ProbabilityTheory.cdf (κ a) q) := by
    …

13. theorem OAI.Problem358.exists_measurable_cdf_kernel_transport line 268

    Source documentation

    Kernel specialization: unique interior CDF fibers suffice for a jointly measurable sampler with the exact conditional law and continuous fibers.

    theorem exists_measurable_cdf_kernel_transport
        {A : Type*} [MeasurableSpace A] (κ : ProbabilityTheory.Kernel A ℝ)
        [ProbabilityTheory.IsMarkovKernel κ]
        (hex : ∀ a t, t ∈ Ioo (0 : ℝ) 1 → ∃! x : ℝ, ProbabilityTheory.cdf (κ a) x = t) :
        ∃ Q : A × ℝ → ℝ, Measurable Q ∧
          (∀ a, Measure.map (fun t => Q (a, t)) (volume.restrict (Ioo (0 : ℝ) 1)) = κ a) ∧
          (∀ a t, t ∈ Ioo (0 : ℝ) 1 → ProbabilityTheory.cdf (κ a) (Q (a, t)) = t) ∧
          ∀ a t, t ∈ Ioo (0 : ℝ) 1 → ContinuousAt (fun s => Q (a, s)) t :=
    …

14. def OAI.Problem358.KernelQuantile.quantile line 299

    Source documentation

    Ordered generalized inverse of the kernel's conditional distribution function.

    def quantile (κ : Kernel X I) (a : X) (t : I) : I :=
    …

15. lemma OAI.Problem358.KernelQuantile.measurable_quantile line 302
16. lemma OAI.Problem358.KernelQuantile.monotone_quantile line 331
17. lemma OAI.Problem358.KernelQuantile.quantile_le_iff line 339

    Source documentation

    The defining order equivalence, including the endpoints of the parameter interval.

    lemma quantile_le_iff (κ : Kernel X I) [IsMarkovKernel κ] (a : X) (ξ x : I) :
        quantile κ a ξ ≤ x ↔ (ξ : ℝ) ≤ (κ a).real (Icc 0 x) := by
    …

    Mentions: OAI.Problem358.KernelQuantile.quantile

18. lemma OAI.Problem358.KernelQuantile.map_quantile line 369
19. theorem OAI.Problem358.KernelQuantile.exists_monotone_unitInterval_sampler line 382

    Source documentation

    Every unit-interval probability kernel has a jointly measurable monotone sampler.

    theorem exists_monotone_unitInterval_sampler (κ : Kernel X I) [IsMarkovKernel κ] :
        ∃ (f : X → I → I), Measurable (uncurry f) ∧ (∀ a, Monotone (f a)) ∧
          ∀ a, volume.map (f a) = κ a :=
    …

20. lemma OAI.Problem358.KernelQuantile.quantile_eq_of_cdf_eq line 388

    Source documentation

    At a strictly increasing conditional CDF, the quantile is its ordinary inverse.

    lemma quantile_eq_of_cdf_eq (κ : Kernel X I) [IsMarkovKernel κ]
        (a : X) (hstrict : StrictMono (fun x : I => (κ a).real (Icc 0 x)))
        {t x : I} (hx : (κ a).real (Icc 0 x) = (t : ℝ)) :
        quantile κ a t = x := by
    …

    Mentions: OAI.Problem358.KernelQuantile.quantile

21. lemma OAI.Problem358.KernelQuantile.quantile_cdf line 398
22. def OAI.Problem358.KernelQuantile.toUnit line 404

    Source documentation

    Clamp affine coordinates into the unit interval.

    def toUnit (l u x : ℝ) : I :=
    …

23. def OAI.Problem358.KernelQuantile.fromUnit line 408

    Source documentation

    Undo affine unit-interval coordinates.

    def fromUnit (l u : ℝ) (t : I) : ℝ := l + (u - l) * (t : ℝ)

24. lemma OAI.Problem358.KernelQuantile.continuous_toUnit line 410
25. lemma OAI.Problem358.KernelQuantile.continuous_fromUnit line 413
26. lemma OAI.Problem358.KernelQuantile.monotone_fromUnit line 417
27. lemma OAI.Problem358.KernelQuantile.fromUnit_toUnit line 423
28. theorem OAI.Problem358.KernelQuantile.exists_monotone_real_sampler line 437

    Source documentation

    Ordered conditional sampling is available uniformly for any kernel supported in a fixed nondegenerate bounded real interval.

    theorem exists_monotone_real_sampler (κ : Kernel X ℝ) [IsMarkovKernel κ]
        (l u : ℝ) (hlu : l < u)
        (hsupp : ∀ a, ∀ᵐ x ∂κ a, x ∈ Icc l u) :
        ∃ f : X → I → ℝ, Measurable (uncurry f) ∧ (∀ a, Monotone (f a)) ∧
          (∀ a, volume.map (f a) = κ a) ∧ (∀ a t, f a t ∈ Icc l u) := by
    …

29. theorem OAI.Problem358.KernelQuantile.exists_monotone_density_sampler line 470

    Source documentation

    A jointly measurable family of normalized bounded densities admits ordered conditional samples. This is the law-producing part of the triangular quantile construction.

    theorem exists_monotone_density_sampler
        (p : X → ℝ → ℝ≥0∞) (hp : Measurable (uncurry p))
        (hnorm : ∀ a, ∫⁻ x, p a x = 1) (l u : ℝ) (hlu : l < u)
        (hsupp : ∀ a x, x ∉ Icc l u → p a x = 0) :
        ∃ f : X → I → ℝ, Measurable (uncurry f) ∧ (∀ a, Monotone (f a)) ∧
          (∀ a, volume.map (f a) = volume.withDensity (p a)) ∧
          (∀ a t, f a t ∈ Icc l u) := by
    …

30. lemma OAI.Problem358.KernelQuantile.cdf_quantile line 496

    Source documentation

    For a continuous strictly increasing CDF with no endpoint atom, sampling inverts that CDF in both directions.

    lemma cdf_quantile (κ : Kernel X I) [IsMarkovKernel κ]
        (a : X) (hstrict : StrictMono (fun x : I => (κ a).real (Icc 0 x)))
        (hcont : Continuous (fun x : I => (κ a).real (Icc 0 x)))
        (hzero : (κ a).real (Icc 0 (0 : I)) = 0) (t : I) :
        (κ a).real (Icc 0 (quantile κ a t)) = (t : ℝ) := by
    …

    Mentions: OAI.Problem358.KernelQuantile.quantile

31. lemma OAI.Problem358.KernelQuantile.strictMono_quantile line 513
32. def OAI.Problem358.PositiveIntervalDensity.clippedCDF line 535

    Source documentation

    The cumulative integral is clamped to its genuine support interval.

    def clippedCDF (D : PositiveIntervalDensity) (x : ℝ) : ℝ :=
    …

    Mentions: OAI.Problem358.PositiveIntervalDensity

33. lemma OAI.Problem358.PositiveIntervalDensity.clippedCDF_of_mem line 538
34. lemma OAI.Problem358.PositiveIntervalDensity.clippedCDF_of_le_lower line 542
35. lemma OAI.Problem358.PositiveIntervalDensity.clippedCDF_of_upper_le line 547
36. lemma OAI.Problem358.PositiveIntervalDensity.clippedCDF_monotone line 552
37. lemma OAI.Problem358.PositiveIntervalDensity.clippedCDF_eq_ite line 559
38. lemma OAI.Problem358.PositiveIntervalDensity.existsUnique_clippedCDF_eq line 568
39. lemma OAI.Problem358.PositiveIntervalDensity.measurable_clippedCDF_section line 587
40. theorem OAI.Problem358.PositiveIntervalDensity.exists_measurable_quantile_family line 600

    Source documentation

    A family of positive interval densities admits a jointly measurable family of exact quantile samplers. Endpoints and cumulative-integral sections must be measurable in the parameter; no parameter differentiability is required.

    theorem exists_measurable_quantile_family {A : Type*} [MeasurableSpace A]
        (D : A → PositiveIntervalDensity)
        (hlower : Measurable (fun a => (D a).lower))
        (hupper : Measurable (fun a => (D a).upper))
        (hcdf : ∀ q : ℝ, Measurable (fun a => (D a).cdf q)) :
        ∃ Q : A × ℝ → ℝ, Measurable Q ∧
          (∀ a t, t ∈ Ioo (0 : ℝ) 1 → Q (a, t) = (D a).quantileReal t) ∧
          (∀ a, Measure.map (fun t => Q (a, t)) (volume.restrict (Ioo (0 : ℝ) 1)) =
            (D a).densityMeasure) ∧
          ∀ a t, t ∈ Ioo (0 : ℝ) 1 →
            HasDerivAt (fun s => Q (a, s)) ((D a).density (Q (a, t)))⁻¹ t := by
    …

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

41. lemma OAI.Problem358.PositiveIntervalDensity.clippedCDF_mem_unitInterval line 652
42. lemma OAI.Problem358.PositiveIntervalDensity.cdf_densityMeasure_eq_clippedCDF line 659

    Source documentation

    The clamped primitive is the actual probability CDF of the density law.

    lemma cdf_densityMeasure_eq_clippedCDF (D : PositiveIntervalDensity) (x : ℝ) :
        ProbabilityTheory.cdf D.densityMeasure x = D.clippedCDF x := by
    …

    Mentions: OAI.Problem358.PositiveIntervalDensity

43. lemma OAI.Problem358.PositiveIntervalDensity.existsUnique_probability_cdf_eq line 689
44. theorem OAI.Problem358.PositiveIntervalDensity.exists_measurable_density_kernel_quantiles line 697

    Source documentation

    A measurable kernel of positive interval-density laws has jointly measurable quantiles with exact conditional laws and inverse-density derivatives. No measurability of chosen support endpoints is separately required.

    theorem exists_measurable_density_kernel_quantiles {A : Type*} [MeasurableSpace A]
        (D : A → PositiveIntervalDensity) (κ : ProbabilityTheory.Kernel A ℝ)
        [ProbabilityTheory.IsMarkovKernel κ]
        (hκ : ∀ a, κ a = (D a).densityMeasure) :
        ∃ Q : A × ℝ → ℝ, Measurable Q ∧
          (∀ a, Measure.map (fun t => Q (a, t)) (volume.restrict (Ioo (0 : ℝ) 1)) = κ a) ∧
          (∀ a t, t ∈ Ioo (0 : ℝ) 1 → Q (a, t) = (D a).quantileReal t) ∧
          ∀ a t, t ∈ Ioo (0 : ℝ) 1 →
            HasDerivAt (fun s => Q (a, s)) ((D a).density (Q (a, t)))⁻¹ t := by
    …

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