AtomicPaths.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem358.atomic_potential_path_L2_bound line 18

Source documentation

The interior potential estimate for an actual linear motion of the sites. All auxiliary boundedness and joint-selector hypotheses of the time-integration theorem are consequences of the positive masses and the energy bounds.

theorem atomic_potential_path_L2_bound
    {d : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι]
    [MeasurableSpace ι] [MeasurableSingletonClass ι]
    (K : Set (E d)) [IsFiniteMeasure (uniformMeasure K)]
    (y z : ι → E d) (m : ι → ℝ) (c r : ι → ℝ → ℝ)
    {w κ : ℝ} {R : ℝ≥0}
    (hw : 0 ≤ w) (hκ : 0 ≤ κ) (hm : ∀ i, 0 < m i)
    (hxR : ∀ᵐ x ∂uniformMeasure K, ‖x‖ ≤ R)
    (hc : ∀ i, Measurable (c i)) (hr : ∀ i, Measurable (r i))
    (hdc : ∀ i t, t ∈ Ioo (0 : ℝ) 1 → HasDerivAt (c i) (r i t) t)
    (hinj : ∀ t ∈ Ioo (0 : ℝ) 1,
      Function.Injective (fun i => (1-t) • y i + t • z i))
…

theorem OAI.Problem358.atomic_potential_path_L2_bound_of_closed_masses line 77

Source documentation

The same actual atomic-motion estimate takes the canonical closed-cell mass equations directly. In particular, existence or measurability of prescribed-mass active selectors is not an additional hypothesis on the intercept path.

theorem atomic_potential_path_L2_bound_of_closed_masses
    {d : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι]
    [MeasurableSpace ι] [MeasurableSingletonClass ι]
    {K : Set (E d)} [IsFiniteMeasure (uniformMeasure K)] (hK : MeasurableSet K)
    (y z : ι → E d) (m : ι → ℝ) (c r : ι → ℝ → ℝ)
    {w κ : ℝ} {R : ℝ≥0}
    (hw : 0 ≤ w) (hκ : 0 ≤ κ) (hm : ∀ i, 0 < m i)
    (hxR : ∀ᵐ x ∂uniformMeasure K, ‖x‖ ≤ R)
    (hc : ∀ i, Measurable (c i)) (hr : ∀ i, Measurable (r i))
    (hdc : ∀ i t, t ∈ Ioo (0 : ℝ) 1 → HasDerivAt (c i) (r i t) t)
    (hinj : ∀ t ∈ Ioo (0 : ℝ) 1,
      Function.Injective (fun i => (1-t) • y i + t • z i))
…

theorem OAI.Problem358.SupportingMapInterpolation.Supports.lipschitzWith line 124
Source documentation
A globally supporting map with bounded values makes its potential Lipschitz. No differentiability or convexity premise is needed for this implication.
```
theorem Supports.lipschitzWith {d : ℕ} {u : E d → ℝ} {T : E d → E d}
    (h : Supports u T) {L : ℝ≥0} (hL : ∀ x, ‖T x‖ ≤ L) :
    LipschitzWith L u := by
…
```
Mentions: OAI.Problem358.SupportingMapInterpolation.Supports

theorem OAI.Problem358.one_third_stability_of_finite_potential_estimate line 145

Source documentation

The exact compact-target stability conclusion reduces to a uniform potential estimate for finite targets. The supplier only gives supporting maps and their laws: optimality, uniqueness, the one-third interpolation, and passage to arbitrary compactly supported probabilities are all proved here.

theorem one_third_stability_of_finite_potential_estimate
    {d : ℕ} {K Y : Set (E d)}
    (hK : IsCompact K) (hKconv : Convex ℝ K)
    (hKint : (interior K).Nonempty) (hY : IsCompact Y) (hYne : Y.Nonempty)
    (L : ℝ≥0) (P : ℝ)
    (hpotential : ∀ (μ ν : Measure (E d)),
      IsProbabilityMeasure μ → IsProbabilityMeasure ν →
      (∃ F : Set (E d), F.Finite ∧ F ⊆ Y ∧ IsSupported μ F) →
      (∃ G : Set (E d), G.Finite ∧ G ⊆ Y ∧ IsSupported ν G) →
      ∃ (u v : E d → ℝ) (T S : E d → E d),
        SupportingMapInterpolation.Supports u T ∧
        SupportingMapInterpolation.Supports v S ∧
…

Mentions: OAI.Problem358.SupportingMapInterpolation.Supports

theorem OAI.Problem358.one_third_stability_of_atomic_potential_estimate line 216

Source documentation

A potential estimate for positive fixed-mass, noncolliding atomic motions implies the full compact-target theorem. The optimal finite coupling, zero-mass deletion, endpoint laws and exact Wasserstein energy are supplied internally.

theorem one_third_stability_of_atomic_potential_estimate
    {d : ℕ} {K Y : Set (E d)}
    (hK : IsCompact K) (hKconv : Convex ℝ K)
    (hKint : (interior K).Nonempty) (hY : IsCompact Y) (hYne : Y.Nonempty)
    (L : ℝ≥0) (hYL : ∀ z ∈ Y, ‖z‖ ≤ L) (P : ℝ)
    (hpotential : ∀ (n : ℕ), 0 < n →
      ∀ (m : Fin n → ℝ) (y z : Fin n → E d),
      (∀ i, 0 < m i) → (∑ i, m i) = 1 →
      (∀ i, ‖y i‖ ≤ L) → (∀ i, ‖z i‖ ≤ L) →
      (∀ t : ℝ, 0 < t → t < 1 →
        Function.Injective (fun i => (1-t) • y i + t • z i)) →
      ∃ (u v : E d → ℝ) (T S : E d → E d),
…