OAI/Analysis/Brenier/NormalizedPaths.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem358.exists_normalized_finite_affine_endpoint_potentials line 18

   Source documentation

   The bounded-energy, normalized interior intercept path itself supplies continuous endpoint potentials with the uniform L² estimate. In particular, no limits or regularity of the original coefficients at times zero and one are assumptions of this theorem.

   theorem exists_normalized_finite_affine_endpoint_potentials
       {d : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι]
       [MeasurableSpace ι] [MeasurableSingletonClass ι]
       (K : Set (E d)) [IsFiniteMeasure (uniformMeasure K)]
       (y v : ι → ℝ → E d) (c r : ι → ℝ → ℝ)
       (active : ℝ × E d → ι) (m : ι → ℝ)
       {w κ : ℝ} {R : ℝ≥0} (hw : 0 ≤ w) (hκ : 0 ≤ κ)
       (hxR : ∀ᵐ x ∂uniformMeasure K, ‖x‖ ≤ R)
       (hpositive : ∀ i, 0 < m i)
       (hy : ∀ i, Continuous (y i))
       (hv : ∀ i, ContinuousOn (v i) (Ioo 0 1))
       (hr : ∀ i, ContinuousOn (r i) (Ioo 0 1))
   …

2. theorem OAI.Problem358.MaxPotential.supports_of_maximizers line 87

   Source documentation

   An everywhere maximizing affine-slope selection supports its finite maximum at every point, including the tie set.

   theorem MaxPotential.supports_of_maximizers
       {ι V : Type*} [Fintype ι] [Nonempty ι]
       [NormedAddCommGroup V] [InnerProductSpace ℝ V]
       (y : ι → V) (c : ι → ℝ) {T : V → V}
       (hactive : ∀ x, ∃ i, T x = y i ∧
         ∀ j, inner ℝ x (y j) + c j ≤ inner ℝ x (y i) + c i) :
       SupportingMapInterpolation.Supports (MaxPotential.potential y c) T := by
   …

   Mentions: OAI.Problem358.SupportingMapInterpolation.Supports, OAI.Problem358.MaxPotential.potential

3. theorem OAI.Problem358.exists_bounded_supporting_finite_affine_endpoint_pair line 103

   Source documentation

   The exact endpoint maps of a continuous finite-affine path have global supporting certificates and inherit the endpoint slope bounds. The interval-law construction is supplied by exists_unique_optimal_finite_affine_path_endpoints; no injectivity or positive individual mass is needed at the endpoints.

   theorem exists_bounded_supporting_finite_affine_endpoint_pair
       {d : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι]
       {K : Set (E d)} (hK : IsCompact K) (hconv : Convex ℝ K)
       (hinterior : (interior K).Nonempty)
       {a b : ℝ} (hab : a < b)
       {y : ℝ → ι → E d} {c : ℝ → ι → ℝ}
       {T : ℝ → E d → E d}
       (w : ι → ℝ≥0∞) (hw : ∑ i, w i = 1)
       (hy : ∀ i, ContinuousOn (fun t => y t i) (Set.Icc a b))
       (hc : ∀ i, ContinuousOn (fun t => c t i) (Set.Icc a b))
       (hTm : ∀ t ∈ Set.Ioo a b, Measurable (T t))
       (hT : ∀ t ∈ Set.Ioo a b, ∀ᵐ x ∂uniformMeasure K,
   …

4. theorem OAI.Problem358.exists_supporting_pair_of_normalized_affine_path line 161

   Source documentation

   A normalized positive-mass affine motion gives the actual endpoint supporting potentials and their exact atomic laws, together with the uniform potential estimate. Neither separation nor intercept limits at the endpoints are assumptions.

   theorem exists_supporting_pair_of_normalized_affine_path
       {d : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι]
       [MeasurableSpace ι] [MeasurableSingletonClass ι]
       {K : Set (E d)} (hK : IsCompact K) (hKconv : Convex ℝ K)
       (hKint : (interior K).Nonempty)
       (y v : ι → ℝ → E d) (c r : ι → ℝ → ℝ)
       (active : ℝ × E d → ι) (m : ι → ℝ)
       {w κ : ℝ} {R L : ℝ≥0} (hw : 0 ≤ w) (hκ : 0 ≤ κ)
       (hxR : ∀ᵐ x ∂uniformMeasure K, ‖x‖ ≤ R)
       (hpositive : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
       (hy : ∀ i, Continuous (y i))
       (hv : ∀ i, ContinuousOn (v i) (Ioo 0 1))
   …

5. theorem OAI.Problem358.exists_supporting_pair_of_closedCell_path line 266

   Source documentation

   The geometric closed-cell mass equations suffice for the endpoint potential pair construction. A common measurable maximizing selector and all its mass identities are derived, not supplied as additional path assumptions.

   theorem exists_supporting_pair_of_closedCell_path
       {d : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι]
       [MeasurableSpace ι] [MeasurableSingletonClass ι]
       {K : Set (E d)} (hK : IsCompact K) (hKconv : Convex ℝ K)
       (hKint : (interior K).Nonempty)
       (y v : ι → ℝ → E d) (c r : ι → ℝ → ℝ) (m : ι → ℝ)
       {w κ : ℝ} {R L : ℝ≥0} (hw : 0 ≤ w) (hκ : 0 ≤ κ)
       (hxR : ∀ᵐ x ∂uniformMeasure K, ‖x‖ ≤ R)
       (hpositive : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
       (hy : ∀ i, Continuous (y i)) (hc : ∀ i, Measurable (c i))
       (hv : ∀ i, ContinuousOn (v i) (Ioo 0 1))
       (hr : ∀ i, ContinuousOn (r i) (Ioo 0 1))
   …