OAI/Analysis/Brenier/CanonicalPaths.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem358.FixedMassIntercepts.exists_canonical_atomic_intercept_path line 17

   Source documentation

   Canonical closed-cell intercepts give the entire normalized path interface: measurability is global, while differentiability and derivative continuity are needed only on the open interval where the sites are distinct.

   theorem exists_canonical_atomic_intercept_path
       {d : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι]
       [MeasurableSpace ι] [MeasurableSingletonClass ι]
       {K : Set (E d)} (hK : IsCompact K) (hconv : Convex ℝ K)
       (hKi : (interior K).Nonempty)
       (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
       (y z : ι → E d) {κ : ℝ} {R : ℝ≥0}
       (hinj : ∀ t ∈ Ioo (0 : ℝ) 1,
         Function.Injective (fun i => (1-t) • y i + t • z i))
       (hregular : ∀ t ∈ Ioo (0 : ℝ) 1,
         ContDiffAt ℝ 1 (fun (q : ℝ) => intercepts hK hconv hKi m hm hsum
           (fun i => (1-q) • y i + q • z i)) t)
   …

   Mentions: OAI.Problem358.FixedMassIntercepts.intercepts

2. theorem OAI.Problem358.FixedMassIntercepts.canonical_atomic_potential_L2_bound_of_deriv_energy line 90

   Source documentation

   The canonical normalized intercept path supplies all measurability and mass hypotheses of the interior potential estimate. Its scalar derivatives are the coordinates of its derivative in the normalization subspace.

   theorem canonical_atomic_potential_L2_bound_of_deriv_energy
       {d : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι]
       [MeasurableSpace ι] [MeasurableSingletonClass ι]
       {K : Set (E d)} (hK : IsCompact K) (hconv : Convex ℝ K)
       (hKi : (interior K).Nonempty)
       (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
       (y z : ι → E d) {w κ : ℝ} {R : ℝ≥0}
       (hw : 0 ≤ w) (hκ : 0 ≤ κ)
       (hbounded : ∀ᵐ x ∂uniformMeasure K, ‖x‖ ≤ R)
       (hinj : ∀ t ∈ Ioo (0 : ℝ) 1,
         Function.Injective (fun i => (1-t) • y i + t • z i))
       (hspeed : (∑ i, m i * ‖z i-y i‖ ^ 2) ≤ w ^ 2)
   …

3. theorem OAI.Problem358.FixedMassIntercepts.exists_actual_atomic_intercept_path line 158

   Source documentation

   Positive prescribed masses along distinct affine site paths admit genuine normalized intercepts with continuous derivatives and the uniform geometric energy bound. All mass regularity and midpoint-coupling inputs are discharged.

   theorem exists_actual_atomic_intercept_path
       {d : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι]
       [MeasurableSpace ι] [MeasurableSingletonClass ι]
       {K : Set (E d)} (hK : IsCompact K) (hconv : Convex ℝ K)
       (hKi : (interior K).Nonempty)
       (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
       (y z : ι → E d) (R : ℝ≥0)
       (hbounded : ∀ᵐ x ∂uniformMeasure K, ‖x‖ ≤ R)
       (hinj : ∀ t ∈ Ioo (0 : ℝ) 1,
         Function.Injective (fun i => (1-t) • y i + t • z i)) :
       ∃ c r : ι → ℝ → ℝ,
         (∀ i, Measurable (c i)) ∧
   …