OAI/Analysis/Brenier/PrefixSampling.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem358.FinitePrefix.stepBody line 15

   Source documentation

   The same body in prefix/next-coordinate/remainder coordinates.

   def stepBody {d n : ℕ} (K : Set (Coordinates d)) (h : n < d) :
       Set (Coordinates n × (ℝ × Coordinates (d-(n+1)))) :=
   …

   Mentions: OAI.Problem358.FinitePrefix.Coordinates

2. lemma OAI.Problem358.FinitePrefix.interior_stepBody line 19
3. lemma OAI.Problem358.FinitePrefix.headBlock_tripleSplit_prefix line 23
4. lemma OAI.Problem358.FinitePrefix.valid_stepBody line 29
5. theorem OAI.Problem358.FinitePrefix.exists_prefix_quantile line 48

   Source documentation

   Each actual finite prefix admits a globally measurable next-coordinate quantile. The conditional law is the precise normalized remaining-body scalar marginal.

   theorem exists_prefix_quantile {d n : ℕ} {K : Set (Coordinates d)}
       (hK : IsCompact K) (hc : Convex ℝ K) (h : n < d) :
       ∃ Q : Coordinates n × ℝ → ℝ, Measurable Q ∧
         (∀ a ∈ prefixDomain K h.le, Measure.map (fun s => Q (a,s))
           (volume.restrict (Ioo (0 : ℝ) 1)) =
           Measure.map Prod.fst
             (((volume.prod volume) (ConvexTriangularSampler.sectionBody (stepBody K h) a))⁻¹ •
               (volume.prod volume).restrict
                 (ConvexTriangularSampler.sectionBody (stepBody K h) a))) ∧
         (∀ a ∈ prefixDomain K h.le, ∀ s ∈ Ioo (0 : ℝ) 1,
           Fin.snoc a (Q (a,s)) ∈ prefixDomain K (Nat.succ_le_of_lt h)) ∧
         (∀ a ∈ prefixDomain K h.le, ∀ s ∈ Ioo (0 : ℝ) 1,
   …

   Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.prefixDomain, OAI.Problem358.ConvexTriangularSampler.sectionBody, OAI.Problem358.FinitePrefix.stepBody

6. def OAI.Problem358.FinitePrefix.bodyQuantileFamily line 98

   Source documentation

   The concrete conditional family, extended by zero beyond the ambient dimension.

   def bodyQuantileFamily {d : ℕ} {K : Set (Coordinates d)}
       (hK : IsCompact K) (hc : Convex ℝ K) : TriangularRecursion.ConditionalFamily :=
   …

   Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.TriangularRecursion.ConditionalFamily

7. lemma OAI.Problem358.FinitePrefix.bodyQuantileFamily_of_lt line 102
8. lemma OAI.Problem358.FinitePrefix.measurable_bodyQuantileFamily line 108
9. lemma OAI.Problem358.FinitePrefix.bodyQuantileFamily_law line 117
10. lemma OAI.Problem358.FinitePrefix.bodyQuantileFamily_mem line 132
11. def OAI.Problem358.FinitePrefix.bodyDerivativeFamily line 142

    Source documentation

    Jointly measurable actual inverse section-density diagonal derivative.

    def bodyDerivativeFamily {d : ℕ} {K : Set (Coordinates d)}
        (hK : IsCompact K) (hc : Convex ℝ K) : TriangularRecursion.ConditionalFamily :=
    …

    Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.TriangularRecursion.ConditionalFamily

12. lemma OAI.Problem358.FinitePrefix.measurable_bodyDerivativeFamily line 148
13. lemma OAI.Problem358.FinitePrefix.bodyQuantileFamily_hasDerivAt line 160
14. lemma OAI.Problem358.FinitePrefix.bodyDerivativeFamily_pos line 172
15. theorem OAI.Problem358.FinitePrefix.bodySample_mem line 190

    Source documentation

    The actual recursively sampled prefix stays in the projection of the body's interior.

    theorem bodySample_mem {d : ℕ} {K : Set (Coordinates d)}
        (hK : IsCompact K) (hc : Convex ℝ K) (hne : (interior K).Nonempty) :
        ∀ n, ∀ h : n ≤ d, ∀ s : Coordinates n,
          TriangularDensity.InUnitCube s →
            TriangularRecursion.sample (bodyQuantileFamily hK hc) n s ∈ prefixDomain K h := by
    …

    Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.TriangularDensity.InUnitCube, OAI.Problem358.TriangularRecursion.sample, OAI.Problem358.FinitePrefix.bodyQuantileFamily, OAI.Problem358.FinitePrefix.prefixDomain

16. theorem OAI.Problem358.FinitePrefix.bodySample_mem_interior line 207

    Source documentation

    The full sampler takes every open unit-cube point into the actual body interior.

    theorem bodySample_mem_interior {d : ℕ} {K : Set (Coordinates d)}
        (hK : IsCompact K) (hc : Convex ℝ K) (hne : (interior K).Nonempty)
        (s : Coordinates d) (hs : TriangularDensity.InUnitCube s) :
        TriangularRecursion.sample (bodyQuantileFamily hK hc) d s ∈ interior K := by
    …

    Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.TriangularDensity.InUnitCube, OAI.Problem358.TriangularRecursion.sample, OAI.Problem358.FinitePrefix.bodyQuantileFamily

17. theorem OAI.Problem358.FinitePrefix.bodySample_fiber_hasDerivAt line 214

    Source documentation

    Derivative regularity along each scalar input of the concrete sampler.

    theorem bodySample_fiber_hasDerivAt {d n : ℕ} {K : Set (Coordinates d)}
        (hK : IsCompact K) (hc : Convex ℝ K) (hne : (interior K).Nonempty)
        (h : n < d) (s : Coordinates n) (hs : TriangularDensity.InUnitCube s)
        (t : ℝ) (ht : t ∈ Ioo (0 : ℝ) 1) :
        HasDerivAt
          (bodyQuantileFamily hK hc n (TriangularRecursion.sample (bodyQuantileFamily hK hc) n s))
          (bodyDerivativeFamily hK hc n (TriangularRecursion.sample (bodyQuantileFamily hK hc) n s) t) t :=
    …

    Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.TriangularDensity.InUnitCube, OAI.Problem358.FinitePrefix.bodyQuantileFamily, OAI.Problem358.TriangularRecursion.sample, OAI.Problem358.FinitePrefix.bodyDerivativeFamily

18. lemma OAI.Problem358.FinitePrefix.bodySample_fiber_derivative_pos line 223
19. lemma OAI.Problem358.FinitePrefix.bodyDerivativeFamily_eq_ratio line 232

    Source documentation

    The concrete derivative is exactly the ratio of consecutive prefix volumes.

    lemma bodyDerivativeFamily_eq_ratio {d n : ℕ} {K : Set (Coordinates d)}
        (hK : IsCompact K) (hc : Convex ℝ K) (h : n < d)
        (a : Coordinates n) (t : ℝ) :
        bodyDerivativeFamily hK hc n a t =
          volume.real (prefixSection K h.le a) /
            volume.real (prefixSection K (Nat.succ_le_of_lt h)
              (Fin.snoc a (bodyQuantileFamily hK hc n a t))) := by
    …

    Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.bodyDerivativeFamily, OAI.Problem358.FinitePrefix.prefixSection, OAI.Problem358.FinitePrefix.bodyQuantileFamily

20. theorem OAI.Problem358.FinitePrefix.bodySample_diagonalProduct_eq_ratio line 244

    Source documentation

    The diagonal derivatives telescope through the actual geometric section volumes.

    theorem bodySample_diagonalProduct_eq_ratio {d : ℕ} {K : Set (Coordinates d)}
        (hK : IsCompact K) (hc : Convex ℝ K) (hne : (interior K).Nonempty) :
        ∀ n, ∀ h : n ≤ d, ∀ s : Coordinates n, TriangularDensity.InUnitCube s →
          TriangularDensity.diagonalProduct (bodyQuantileFamily hK hc)
            (bodyDerivativeFamily hK hc) n s =
              (volume K).toReal /
                volume.real (prefixSection K h
                  (TriangularRecursion.sample (bodyQuantileFamily hK hc) n s)) := by
    …

    Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.TriangularDensity.InUnitCube, OAI.Problem358.TriangularDensity.diagonalProduct, OAI.Problem358.FinitePrefix.bodyQuantileFamily, OAI.Problem358.FinitePrefix.bodyDerivativeFamily, OAI.Problem358.FinitePrefix.prefixSection, OAI.Problem358.TriangularRecursion.sample

21. theorem OAI.Problem358.FinitePrefix.bodySample_diagonalProduct_eq_volume line 280

    Source documentation

    The full Jacobian product is the body's volume, with no seed dependence.

    theorem bodySample_diagonalProduct_eq_volume {d : ℕ} {K : Set (Coordinates d)}
        (hK : IsCompact K) (hc : Convex ℝ K) (hne : (interior K).Nonempty)
        (s : Coordinates d) (hs : TriangularDensity.InUnitCube s) :
        TriangularDensity.diagonalProduct (bodyQuantileFamily hK hc)
          (bodyDerivativeFamily hK hc) d s = (volume K).toReal := by
    …

    Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.TriangularDensity.InUnitCube, OAI.Problem358.TriangularDensity.diagonalProduct, OAI.Problem358.FinitePrefix.bodyQuantileFamily, OAI.Problem358.FinitePrefix.bodyDerivativeFamily

22. def OAI.Problem358.FinitePrefix.prefixLaw line 302

    Source documentation

    The actual first-coordinate marginal of normalized volume on the body.

    def prefixLaw {d n : ℕ} (K : Set (Coordinates d)) (h : n ≤ d) :
        Measure (Coordinates n) :=
    …

    Mentions: OAI.Problem358.FinitePrefix.Coordinates

23. theorem OAI.Problem358.FinitePrefix.prefixLaw_density line 306
24. theorem OAI.Problem358.FinitePrefix.isProbabilityMeasure_normalizedVolume line 312
25. theorem OAI.Problem358.FinitePrefix.isProbabilityMeasure_prefixLaw line 321
26. theorem OAI.Problem358.FinitePrefix.prefixLaw_full line 328
27. theorem OAI.Problem358.FinitePrefix.measurableSet_stepBody line 333
28. theorem OAI.Problem358.FinitePrefix.volume_stepBody line 337
29. theorem OAI.Problem358.FinitePrefix.map_tripleSplit_normalized line 341
30. theorem OAI.Problem358.FinitePrefix.prefixLaw_eq_step_fst line 350
31. theorem OAI.Problem358.FinitePrefix.prefixLaw_succ_eq_step_map line 362
32. def OAI.Problem358.FinitePrefix.prefixKernel line 377

    Source documentation

    The next-coordinate conditional law, completed by a point on null prefixes.

    def prefixKernel {d n : ℕ} {K : Set (Coordinates d)}
        (hK : MeasurableSet K) (h : n < d) : Kernel (Coordinates n) ℝ :=
    …

    Mentions: OAI.Problem358.FinitePrefix.Coordinates

33. theorem OAI.Problem358.FinitePrefix.isMarkovKernel_prefixKernel line 383
34. theorem OAI.Problem358.FinitePrefix.prefixKernel_apply_valid line 390
35. theorem OAI.Problem358.FinitePrefix.prefixLaw_compProd_prefixKernel line 417
36. theorem OAI.Problem358.FinitePrefix.prefixLaw_succ line 446

    Source documentation

    Genuine one-step disintegration of the geometric prefix laws.

    theorem prefixLaw_succ {d n : ℕ} {K : Set (Coordinates d)}
        (hK : IsCompact K) (hi : (interior K).Nonempty) (h : n < d) :
        prefixLaw K (Nat.succ_le_of_lt h) =
          Measure.map (fun p : Coordinates n × ℝ => Fin.snoc p.1 p.2)
            ((prefixLaw K h.le).compProd (prefixKernel hK.measurableSet h)) := by
    …

    Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.prefixLaw, OAI.Problem358.FinitePrefix.prefixKernel

37. theorem OAI.Problem358.FinitePrefix.bodyMidpoint_smul_map_le_volume line 470

    Source documentation

    The midpoint of the two actual convex-body samplers has the sharp geometric volume domination. All scalar differentiability, prefix support, measurability, and terminal Jacobian identities are consequences of the two bodies.

    theorem bodyMidpoint_smul_map_le_volume
        {d : ℕ} {K L : Set (Coordinates d)}
        (hK : IsCompact K) (hcK : Convex ℝ K) (hiK : (interior K).Nonempty)
        (hL : IsCompact L) (hcL : Convex ℝ L) (hiL : (interior L).Nonempty) :
        ENNReal.ofReal (Real.sqrt ((volume K).toReal * (volume L).toReal)) •
          Measure.map (midpoint (bodyQuantileFamily hK hcK) (bodyQuantileFamily hL hcL) d)
            (Measure.pi fun _ : Fin d => volume.restrict (Ioo (0 : ℝ) 1)) ≤
          (volume : Measure (Coordinates d)) := by
    …

    Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.bodyQuantileFamily

38. theorem OAI.Problem358.FinitePrefix.bodyMidpoint_smul_map_le_volume_of_pos line 498

    Source documentation

    Positive volume is sufficient for the geometric body hypotheses; no chosen interior point is required in this form of the domination theorem.

    theorem bodyMidpoint_smul_map_le_volume_of_pos
        {d : ℕ} {K L : Set (Coordinates d)}
        (hK : IsCompact K) (hcK : Convex ℝ K) (hvK : 0 < volume K)
        (hL : IsCompact L) (hcL : Convex ℝ L) (hvL : 0 < volume L) :
        ENNReal.ofReal (Real.sqrt ((volume K).toReal * (volume L).toReal)) •
          Measure.map (midpoint (bodyQuantileFamily hK hcK) (bodyQuantileFamily hL hcL) d)
            (Measure.pi fun _ : Fin d => volume.restrict (Ioo (0 : ℝ) 1)) ≤
          (volume : Measure (Coordinates d)) := by
    …

    Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.bodyQuantileFamily

39. theorem OAI.Problem358.FinitePrefix.map_bodyQuantile_sample_prefix line 529

    Source documentation

    Every stage of the actual convex-body quantile construction has the corresponding geometric prefix marginal.

    theorem map_bodyQuantile_sample_prefix {d : ℕ} {K : Set (Coordinates d)}
        (hK : IsCompact K) (hc : Convex ℝ K) (hi : (interior K).Nonempty) :
        ∀ n (h : n ≤ d),
          Measure.map (TriangularRecursion.sample (bodyQuantileFamily hK hc) n)
            (Measure.pi (fun _ : Fin n => volume.restrict (Ioo (0 : ℝ) 1))) =
              prefixLaw K h := by
    …

    Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.TriangularRecursion.sample, OAI.Problem358.FinitePrefix.bodyQuantileFamily, OAI.Problem358.FinitePrefix.prefixLaw

40. theorem OAI.Problem358.FinitePrefix.map_bodyQuantile_sample line 578

    Source documentation

    The concrete, globally measurable triangular quantile sampler has exactly the uniform probability law of the convex body.

    theorem map_bodyQuantile_sample {d : ℕ} {K : Set (Coordinates d)}
        (hK : IsCompact K) (hc : Convex ℝ K) (hi : (interior K).Nonempty) :
        Measure.map (TriangularRecursion.sample (bodyQuantileFamily hK hc) d)
          (Measure.pi (fun _ : Fin d => volume.restrict (Ioo (0 : ℝ) 1))) =
            (volume K)⁻¹ • volume.restrict K := by
    …

    Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.TriangularRecursion.sample, OAI.Problem358.FinitePrefix.bodyQuantileFamily

41. lemma OAI.Problem358.convex_interior_nonempty_of_volume_pos line 596

    Source documentation

    A convex body of positive volume has a nonempty interior.

    lemma convex_interior_nonempty_of_volume_pos {d : ℕ} {K : Set (E d)}
        (hc : Convex ℝ K) (hvol : 0 < volume K) : (interior K).Nonempty := by
    …

42. lemma OAI.Problem358.coordinate_body_geometry line 605

    Source documentation

    All body hypotheses survive the canonical volume-preserving Euclidean coordinate map.

    lemma coordinate_body_geometry {d : ℕ} {K : Set (E d)}
        (hK : IsCompact K) (hc : Convex ℝ K) (hne : (interior K).Nonempty) :
        IsCompact ((WithLp.toLp 2) ⁻¹' K) ∧
          Convex ℝ ((WithLp.toLp 2) ⁻¹' K) ∧
          (interior ((WithLp.toLp 2) ⁻¹' K)).Nonempty := by
    …

43. theorem OAI.Problem358.exists_convexBody_midpoint_coupling line 620

    Source documentation

    Every pair of compact convex bodies admits a uniform coupling whose midpoint law is dominated by volume with the geometric-mean volume factor.

    theorem exists_convexBody_midpoint_coupling {d : ℕ} {K L : Set (E d)}
        (hK : IsCompact K) (hcK : Convex ℝ K) (hiK : (interior K).Nonempty)
        (hL : IsCompact L) (hcL : Convex ℝ L) (hiL : (interior L).Nonempty) :
        ∃ π : Measure (E d × E d), IsCoupling (uniformMeasure K) (uniformMeasure L) π ∧
          ENNReal.ofReal (Real.sqrt ((volume K).toReal * (volume L).toReal)) •
            Measure.map (fun p : E d × E d => (1 / 2 : ℝ) • (p.1 + p.2)) π ≤ volume := by
    …

44. theorem OAI.Problem358.exists_convexBody_midpoint_coupling_of_pos line 649

    Source documentation

    Positive volume suffices, including in dimension zero.

    theorem exists_convexBody_midpoint_coupling_of_pos {d : ℕ} {K L : Set (E d)}
        (hK : IsCompact K) (hcK : Convex ℝ K) (hvK : 0 < volume K)
        (hL : IsCompact L) (hcL : Convex ℝ L) (hvL : 0 < volume L) :
        ∃ π : Measure (E d × E d), IsCoupling (uniformMeasure K) (uniformMeasure L) π ∧
          ENNReal.ofReal (Real.sqrt ((volume K).toReal * (volume L).toReal)) •
            Measure.map (fun p : E d × E d => (1 / 2 : ℝ) • (p.1 + p.2)) π ≤ volume :=
    …