OAI/Analysis/Brenier/ConvexQuantiles.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem358.AffineSlice.normalizedBodyKernel line 16

   Source documentation

   Normalized restrictions of a jointly measurable family form a kernel. No normalization assertion is made at zero or infinite mass.

   def normalizedBodyKernel {A B : Type*} [MeasurableSpace A] [MeasurableSpace B]
       (ν : Measure B) [SFinite ν] (K : A → Set B)
       (hK : MeasurableSet {p : A × B | p.2 ∈ K p.1}) : Kernel A B where
   …

2. theorem OAI.Problem358.AffineSlice.normalizedBodyKernel_apply line 30
3. theorem OAI.Problem358.AffineSlice.normalizedBodyKernel_isMarkov line 35
4. theorem OAI.Problem358.AffineSlice.exists_measurable_scalar_quantile_family_of_convex_body line 51

   Source documentation

   Jointly measurable exact scalar quantiles for a measurable family of compact convex bodies. Support endpoints need not be chosen measurably. The derivative and law use the actual section volumes of each body.

   theorem exists_measurable_scalar_quantile_family_of_convex_body
       {A V : Type*} [MeasurableSpace A]
       [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V]
       [MeasurableSpace V] [BorelSpace V]
       (μ : Measure V) [IsAddHaarMeasure μ]
       (K : A → Set (ℝ × V))
       (hfamily : MeasurableSet {p : A × (ℝ × V) | p.2 ∈ K p.1})
       (hcompact : ∀ a, IsCompact (K a))
       (hconvex : ∀ a, Convex ℝ (K a))
       (hinterior : ∀ a, (interior (K a)).Nonempty) :
       ∃ Q : A × ℝ → ℝ, Measurable Q ∧
         (∀ a s, s ∈ Ioo (0 : ℝ) 1 → Q (a, s) ∈ Prod.fst '' interior (K a)) ∧
   …

5. theorem OAI.Problem358.AffineSlice.convex_fiber line 107

   Source documentation

   Taking a prefix section preserves convexity.

   theorem convex_fiber {K : Set (U × V)} (hK : Convex ℝ K) (p : U) :
       Convex ℝ (fiber K p) :=
   …

   Mentions: OAI.Problem358.AffineSlice.fiber

6. theorem OAI.Problem358.AffineSlice.interior_fiber_eq line 112

   Source documentation

   At valid prefixes, interior and section commute exactly.

   theorem interior_fiber_eq {K : Set (U × V)} (hK : Convex ℝ K)
       {p : U} (hp : ∃ v : V, (p, v) ∈ interior K) :
       interior (fiber K p) = fiber (interior K) p := by
   …

   Mentions: OAI.Problem358.AffineSlice.fiber

7. theorem OAI.Problem358.AffineSlice.prefix_section_body line 120

   Source documentation

   A valid prefix section remains a full-dimensional compact convex body.

   theorem prefix_section_body {K : Set (U × V)} (hK : IsCompact K)
       (hconv : Convex ℝ K) {p : U} (hp : ∃ v : V, (p, v) ∈ interior K) :
       IsCompact (fiber K p) ∧ Convex ℝ (fiber K p) ∧
         (interior (fiber K p)).Nonempty := by
   …

   Mentions: OAI.Problem358.AffineSlice.fiber

8. theorem OAI.Problem358.AffineSlice.mem_projection_interior_fiber_iff line 130

   Source documentation

   Membership in the next scalar projection means precisely that the extended prefix admits an interior completion.

   theorem mem_projection_interior_fiber_iff {K : Set (U × (ℝ × V))}
       (hconv : Convex ℝ K) {p : U} (hp : ∃ z : ℝ × V, (p, z) ∈ interior K)
       (t : ℝ) :
       t ∈ Prod.fst '' interior (fiber K p) ↔ ∃ v : V, (p, (t, v)) ∈ interior K := by
   …

   Mentions: OAI.Problem358.AffineSlice.fiber

9. theorem OAI.Problem358.AffineSlice.exists_positiveIntervalDensity_of_prefix line 147

   Source documentation

   Every valid prefix supplies an actual positive scalar density, with its support equal to the valid next-prefix interval. No geometric premise remains.

   theorem exists_positiveIntervalDensity_of_prefix
       (μ : Measure V) [IsAddHaarMeasure μ]
       {K : Set (U × (ℝ × V))} (hK : IsCompact K) (hconv : Convex ℝ K)
       {p : U} (hp : ∃ z : ℝ × V, (p, z) ∈ interior K) :
       ∃ D : PositiveIntervalDensity,
         D.density = (fun t => μ.real (fiber (fiber K p) t) /
           (volume.prod μ).real (fiber K p)) ∧
         (∀ t : ℝ, t ∈ Ioo D.lower D.upper ↔ ∃ v : V, (p, (t, v)) ∈ interior K) ∧
         D.densityMeasure = Measure.map Prod.fst
           (((volume.prod μ) (fiber K p))⁻¹ • (volume.prod μ).restrict (fiber K p)) := by
   …

   Mentions: OAI.Problem358.PositiveIntervalDensity, OAI.Problem358.AffineSlice.fiber

10. theorem OAI.Problem358.AffineSlice.exists_scalar_quantile_of_prefix line 166

    Source documentation

    Quantile recursion preserves valid prefixes and has the exact sectional law and telescoping inverse-density derivative.

    theorem exists_scalar_quantile_of_prefix
        (μ : Measure V) [IsAddHaarMeasure μ]
        {K : Set (U × (ℝ × V))} (hK : IsCompact K) (hconv : Convex ℝ K)
        {p : U} (hp : ∃ z : ℝ × V, (p, z) ∈ interior K) :
        ∃ Q : ℝ → ℝ, Continuous Q ∧
          (∀ s ∈ Ioo (0 : ℝ) 1, ∃ v : V, (p, (Q s, v)) ∈ interior K) ∧
          (∀ s ∈ Ioo (0 : ℝ) 1, HasDerivAt Q
            ((volume.prod μ).real (fiber K p) / μ.real (fiber (fiber K p) (Q s))) s) ∧
          Measure.map Q (volume.restrict (Ioo (0 : ℝ) 1)) =
            Measure.map Prod.fst
              (((volume.prod μ) (fiber K p))⁻¹ • (volume.prod μ).restrict (fiber K p)) := by
    …

    Mentions: OAI.Problem358.AffineSlice.fiber

11. def OAI.Problem358.ConvexTriangularSampler.valid line 199

    Source documentation

    Prefixes whose remaining section meets the interior of the body.

    def valid (K : Set (U × (ℝ × V))) : Set U := Prod.fst '' interior K

12. def OAI.Problem358.ConvexTriangularSampler.sectionBody line 202

    Source documentation

    The remaining compact body after fixing a valid prefix.

    def sectionBody (K : Set (U × (ℝ × V))) (x : U) : Set (ℝ × V) :=
    …

13. lemma OAI.Problem358.ConvexTriangularSampler.isOpen_valid line 208
14. lemma OAI.Problem358.ConvexTriangularSampler.isCompact_sectionBody line 214
15. lemma OAI.Problem358.ConvexTriangularSampler.convex_sectionBody line 219
16. lemma OAI.Problem358.ConvexTriangularSampler.sectionBody_interior_nonempty line 226
17. lemma OAI.Problem358.ConvexTriangularSampler.interior_sectionBody line 237
18. def OAI.Problem358.ConvexTriangularSampler.conditionalDensity line 254

    Source documentation

    The density is chosen only after its concrete geometric existence has been proved.

    @[irreducible] def conditionalDensity (x : valid K) : PositiveIntervalDensity :=
    …

    Mentions: OAI.Problem358.ConvexTriangularSampler.valid, OAI.Problem358.PositiveIntervalDensity

19. lemma OAI.Problem358.ConvexTriangularSampler.conditionalDensity_spec line 260
20. def OAI.Problem358.ConvexTriangularSampler.conditionalQuantile line 272

    Source documentation

    Actual conditional inverse-CDF sampling on a valid convex prefix.

    def conditionalQuantile (x : valid K) : ℝ → ℝ :=
    …

    Mentions: OAI.Problem358.ConvexTriangularSampler.valid

21. lemma OAI.Problem358.ConvexTriangularSampler.conditionalQuantile_mem line 276
22. lemma OAI.Problem358.ConvexTriangularSampler.conditionalQuantile_hasDerivAt line 286
23. lemma OAI.Problem358.ConvexTriangularSampler.map_conditionalQuantile line 296
24. def OAI.Problem358.ConvexTriangularSampler.sectionDensity line 307

    Source documentation

    The concrete section-density ratio is jointly measurable even at invalid prefixes.

    def sectionDensity (K : Set (U × (ℝ × V))) (μ : Measure V) (x : U) (t : ℝ) : ℝ :=
    …

25. lemma OAI.Problem358.ConvexTriangularSampler.measurable_sectionDensity line 313
26. lemma OAI.Problem358.ConvexTriangularSampler.conditionalDensity_density line 325
27. def OAI.Problem358.ConvexTriangularSampler.scalarDomain line 330

    Source documentation

    The open set of valid prefixes extended by one scalar coordinate.

    def scalarDomain (K : Set (U × (ℝ × V))) : Set (U × ℝ) :=
    …

28. lemma OAI.Problem358.ConvexTriangularSampler.isOpen_scalarDomain line 336
29. lemma OAI.Problem358.ConvexTriangularSampler.mem_scalarDomain line 342
30. lemma OAI.Problem358.ConvexTriangularSampler.projection_scalarDomain line 355
31. lemma OAI.Problem358.ConvexTriangularSampler.fiber_scalarDomain line 367
32. theorem OAI.Problem358.ConvexTriangularSampler.exists_measurable_conditional_quantile line 382

    Source documentation

    A compact convex body has a globally jointly measurable conditional scalar sampler. Its law, derivative and interior support are all derived from the body itself.

    theorem exists_measurable_conditional_quantile (hK : IsCompact K) (hc : Convex ℝ K) :
        ∃ Q : U × ℝ → ℝ, Measurable Q ∧
          (∀ x ∈ valid K, Measure.map (fun s => Q (x,s))
            (volume.restrict (Ioo (0 : ℝ) 1)) =
            Measure.map Prod.fst (((volume.prod μ) (sectionBody K x))⁻¹ •
              (volume.prod μ).restrict (sectionBody K x))) ∧
          (∀ x ∈ valid K, ∀ s ∈ Ioo (0 : ℝ) 1,
            ∃ z : V, (x,(Q (x,s),z)) ∈ interior K) ∧
          (∀ x ∈ valid K, ∀ s ∈ Ioo (0 : ℝ) 1,
            HasDerivAt (fun t => Q (x,t))
              ((volume.prod μ).real (sectionBody K x) /
                μ.real (AffineSlice.fiber (sectionBody K x) (Q (x,s)))) s) ∧
    …

    Mentions: OAI.Problem358.ConvexTriangularSampler.valid, OAI.Problem358.ConvexTriangularSampler.sectionBody, OAI.Problem358.AffineSlice.fiber

33. def OAI.Problem358.AffineSlice.interiorPrefix line 444

    Source documentation

    Prefixes admitting an interior completion in the body.

    def interiorPrefix (K : Set (U × V)) : Set U :=
    …

34. theorem OAI.Problem358.AffineSlice.exists_measurable_scalar_quantile_family_of_prefix line 452

    Source documentation

    A compact convex body supplies the jointly measurable conditional quantiles on every valid prefix, with actual fiber laws and no endpoint measurability premise.

    theorem exists_measurable_scalar_quantile_family_of_prefix
        (μ : Measure V) [IsAddHaarMeasure μ]
        {K : Set (U × (ℝ × V))} (hK : IsCompact K) (hconv : Convex ℝ K) :
        ∃ Q : interiorPrefix K × ℝ → ℝ, Measurable Q ∧
          (∀ (p : interiorPrefix K) s, s ∈ Ioo (0 : ℝ) 1 →
            ∃ v : V, ((p : U), (Q (p, s), v)) ∈ interior K) ∧
          (∀ (p : interiorPrefix K) s, s ∈ Ioo (0 : ℝ) 1 → HasDerivAt (fun t => Q (p, t))
            ((volume.prod μ).real (fiber K (p : U)) /
              μ.real (fiber (fiber K (p : U)) (Q (p, s)))) s) ∧
          ∀ (p : interiorPrefix K), Measure.map (fun t => Q (p, t)) (volume.restrict (Ioo (0 : ℝ) 1)) =
            Measure.map Prod.fst
              (((volume.prod μ) (fiber K (p : U)))⁻¹ •
    …

    Mentions: OAI.Problem358.AffineSlice.interiorPrefix, OAI.Problem358.AffineSlice.fiber