OAI/Analysis/Brenier/ConvexDensity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem358.AffineSlice.exists_projection_interval line 19

   Source documentation

   The scalar projection of a convex body's interior is a bounded open interval, and its whole projection lies in the corresponding closed interval.

   theorem exists_projection_interval {K : Set (ℝ × V)} (hK : IsCompact K)
       (hconv : Convex ℝ K) (hne : (interior K).Nonempty) :
       ∃ a b : ℝ, a < b ∧ Prod.fst '' interior K = Ioo a b ∧
         Prod.fst '' K ⊆ Icc a b := by
   …

2. theorem OAI.Problem358.AffineSlice.integral_fiberMeasureReal line 46

   Source documentation

   Fubini identity for the real-valued volume of compact fibers.

   theorem integral_fiberMeasureReal (μ : Measure V) [IsAddHaarMeasure μ]
       {K : Set (ℝ × V)} (hK : IsCompact K) :
       (∫ t, μ.real (fiber K t)) = (volume.prod μ).real K := by
   …

   Mentions: OAI.Problem358.AffineSlice.fiber

3. theorem OAI.Problem358.AffineSlice.integrable_fiberMeasureReal line 57
4. theorem OAI.Problem358.AffineSlice.exists_positiveIntervalDensity_of_convex_body line 66

   Source documentation

   A compact convex body supplies an actual positive normalized 1D section density.

   theorem exists_positiveIntervalDensity_of_convex_body
       (μ : Measure V) [IsAddHaarMeasure μ]
       {K : Set (ℝ × V)} (hK : IsCompact K) (hconv : Convex ℝ K)
       (hne : (interior K).Nonempty) :
       ∃ D : PositiveIntervalDensity,
         D.density = (fun t => μ.real (fiber K t) / (volume.prod μ).real K) ∧
         Ioo D.lower D.upper = Prod.fst '' interior K := by
   …

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

5. theorem OAI.Problem358.AffineSlice.densityMeasure_eq_scalar_marginal line 112

   Source documentation

   The density object obtained from a convex body has exactly its scalar marginal law.

   theorem densityMeasure_eq_scalar_marginal
       (μ : Measure V) [IsAddHaarMeasure μ]
       {K : Set (ℝ × V)} (hK : IsCompact K) (hconv : Convex ℝ K)
       (hne : (interior K).Nonempty) (D : PositiveIntervalDensity)
       (hden : D.density = fun t => μ.real (fiber K t) / (volume.prod μ).real K)
       (hI : Ioo D.lower D.upper = Prod.fst '' interior K) :
       D.densityMeasure = Measure.map Prod.fst
         (((volume.prod μ) K)⁻¹ • (volume.prod μ).restrict K) := by
   …

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

6. theorem OAI.Problem358.AffineSlice.exists_scalar_quantile_of_convex_body line 155

   Source documentation

   A scalar conditional quantile with its actual body marginal, not merely an abstract density law.

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

   Mentions: OAI.Problem358.AffineSlice.fiber

7. theorem OAI.Problem358.PositiveIntervalDensity.measurable_endpoints_of_open_fibers line 191

   Source documentation

   The endpoints of any chosen interval-density description are measurable when the intervals are precisely the fibers of an open set. No measurability of the choice of density bundles is needed.

   theorem measurable_endpoints_of_open_fibers {A : Type*} [TopologicalSpace A]
       [MeasurableSpace A] [OpensMeasurableSpace A]
       {U : Set (A × ℝ)} (hU : IsOpen U)
       (D : (Prod.fst '' U) → PositiveIntervalDensity)
       (hsupport : ∀ a, Ioo (D a).lower (D a).upper = SectionMeasure.fiber U a.val) :
       Measurable (fun a => (D a).lower) ∧ Measurable (fun a => (D a).upper) := by
   …

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

8. theorem OAI.Problem358.PositiveIntervalDensity.exists_quantiles_of_open_fiber_densities line 220

   Source documentation

   Existential positive-density data on each open scalar fiber already determine a jointly measurable family of actual quantile transports. In particular arbitrary choices of the scalar density bundles do not leave a parameter-measurability gap.

   theorem exists_quantiles_of_open_fiber_densities {A : Type*} [TopologicalSpace A]
       [MeasurableSpace A] [OpensMeasurableSpace A]
       {U : Set (A × ℝ)} (hU : IsOpen U) (p : A × ℝ → ℝ) (hp : Measurable p)
       (hex : ∀ a : Prod.fst '' U, ∃ D : PositiveIntervalDensity,
         D.density = (fun t => p (a.val, t)) ∧
         Ioo D.lower D.upper = SectionMeasure.fiber U a.val) :
       ∃ Q : A × ℝ → ℝ, Measurable Q ∧
         (∀ a : Prod.fst '' U, Measure.map (fun s => Q (a.val, s))
           (volume.restrict (Ioo (0 : ℝ) 1)) =
             (volume.restrict (SectionMeasure.fiber U a.val)).withDensity
               (fun t => ENNReal.ofReal (p (a.val, t)))) ∧
         (∀ a : Prod.fst '' U, ∀ s ∈ Ioo (0 : ℝ) 1, (a.val, Q (a.val, s)) ∈ U) ∧
   …

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