EndpointEnergy.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Bounded intercept speeds give finite endpoint values in the moving-site argument.

theorem OAI.Problem358.intercept_lipschitzOn line 15

Source documentation

A differentiable intercept with uniformly bounded speed is Lipschitz on its open parameter interval. No value or continuity at either endpoint is assumed.

theorem intercept_lipschitzOn {a b : ℝ} {c c' : ℝ → ℝ} {L : ℝ≥0}
    (hderiv : ∀ t ∈ Ioo a b, HasDerivAt c (c' t) t)
    (hbound : ∀ t ∈ Ioo a b, |c' t| ≤ L) :
    LipschitzOnWith L c (Ioo a b) := by
…

theorem OAI.Problem358.exists_intercept_extension line 26

Source documentation

An intercept with bounded speed admits a globally Lipschitz extension from the open parameter interval. This is used only for endpoint existence.

theorem exists_intercept_extension {a b : ℝ} {c c' : ℝ → ℝ} {L : ℝ≥0}
    (hderiv : ∀ t ∈ Ioo a b, HasDerivAt c (c' t) t)
    (hbound : ∀ t ∈ Ioo a b, |c' t| ≤ L) :
    ∃ g : ℝ → ℝ, LipschitzWith L g ∧ EqOn c g (Ioo a b) :=
…

theorem OAI.Problem358.intercept_endpoint_limits line 34

Source documentation

The original intercept tends to the values of any continuous extension at both endpoints, from inside the parameter interval.

theorem intercept_endpoint_limits {a b : ℝ} (hab : a < b) {c g : ℝ → ℝ}
    (hg : Continuous g) (hcg : EqOn c g (Ioo a b)) :
    Tendsto c (𝓝[>] a) (𝓝 (g a)) ∧ Tendsto c (𝓝[<] b) (𝓝 (g b)) := by
…

theorem OAI.Problem358.exists_intercept_endpoint_limits line 46

Source documentation

Finite one-sided endpoint limits follow directly from the derivative bound.

theorem exists_intercept_endpoint_limits {a b : ℝ} (hab : a < b)
    {c c' : ℝ → ℝ} {L : ℝ≥0}
    (hderiv : ∀ t ∈ Ioo a b, HasDerivAt c (c' t) t)
    (hbound : ∀ t ∈ Ioo a b, |c' t| ≤ L) :
    ∃ ca cb : ℝ, Tendsto c (𝓝[>] a) (𝓝 ca) ∧
      Tendsto c (𝓝[<] b) (𝓝 cb) ∧ |cb - ca| ≤ L * (b - a) := by
…

theorem OAI.Problem358.exists_finite_intercept_extensions line 58

Source documentation

The extensions can be chosen simultaneously for a finite family of intercepts.

theorem exists_finite_intercept_extensions {ι : Type*} {a b : ℝ}
    {c c' : ι → ℝ → ℝ} {L : ι → ℝ≥0}
    (hderiv : ∀ i t, t ∈ Ioo a b → HasDerivAt (c i) (c' i t) t)
    (hbound : ∀ i t, t ∈ Ioo a b → |c' i t| ≤ L i) :
    ∃ g : ι → ℝ → ℝ, ∀ i, LipschitzWith (L i) (g i) ∧ EqOn (c i) (g i) (Ioo a b) := by
…

theorem OAI.Problem358.intercept_normalization_closed line 67

Source documentation

Weighted normalization on the interior persists at both endpoints of a continuous family. This avoids any mass-dependent endpoint estimate.

theorem intercept_normalization_closed {ι : Type*} [Fintype ι]
    {a b : ℝ} (hab : a < b) (m : ι → ℝ) {g : ι → ℝ → ℝ}
    (hg : ∀ i, Continuous (g i))
    (hnorm : ∀ t ∈ Ioo a b, ∑ i, m i * g i t = 0) :
    ∀ t ∈ Icc a b, ∑ i, m i * g i t = 0 := by
…

theorem OAI.Problem358.InterceptEndpointExtension.abs_le_sqrt_energy_div_mass line 92
Source documentation
A positive weighted quadratic-energy bound controls every coordinate. The mass dependence is used only to construct endpoint intercepts.
```
theorem abs_le_sqrt_energy_div_mass
    {ι : Type*} [Fintype ι] (m r : ι → ℝ) {energy : ℝ}
    (hm : ∀ i, 0 < m i)
    (henergy : (∑ i, m i * r i ^ 2) ≤ energy) (i : ι) :
    |r i| ≤ Real.sqrt (energy / m i) := by
…
```

theorem OAI.Problem358.InterceptEndpointExtension.lipschitzOnWith_of_weighted_derivative_energy line 109

Source documentation

Intercept derivatives with a uniform weighted energy bound give a coordinatewise Lipschitz estimate on the entire open time interval.

theorem lipschitzOnWith_of_weighted_derivative_energy
    {ι : Type*} [Fintype ι] (m : ι → ℝ) (c r : ι → ℝ → ℝ)
    {a b energy : ℝ} (hm : ∀ i, 0 < m i)
    (hderiv : ∀ i t, t ∈ Ioo a b → HasDerivAt (c i) (r i t) t)
    (henergy : ∀ t ∈ Ioo a b, (∑ i, m i * r i t ^ 2) ≤ energy)
    (i : ι) :
    LipschitzOnWith ⟨Real.sqrt (energy / m i), Real.sqrt_nonneg _⟩ (c i) (Ioo a b) := by
…

theorem OAI.Problem358.InterceptEndpointExtension.exists_lipschitz_extension line 126

Source documentation

A fixed-mass intercept path with bounded weighted derivative energy has continuous endpoint values. The extension agrees on the interior and has the same interior derivatives. No separation of endpoint sites is required.

theorem exists_lipschitz_extension
    {ι : Type*} [Fintype ι] (m : ι → ℝ) (c r : ι → ℝ → ℝ)
    {a b energy : ℝ} (hm : ∀ i, 0 < m i)
    (hderiv : ∀ i t, t ∈ Ioo a b → HasDerivAt (c i) (r i t) t)
    (henergy : ∀ t ∈ Ioo a b, (∑ i, m i * r i t ^ 2) ≤ energy) :
    ∃ C : ι → ℝ → ℝ,
      (∀ i, LipschitzWith ⟨Real.sqrt (energy / m i), Real.sqrt_nonneg _⟩ (C i)) ∧
      (∀ i, EqOn (c i) (C i) (Ioo a b)) ∧
      (∀ i t, t ∈ Ioo a b → HasDerivAt (C i) (r i t) t) := by
…

theorem OAI.Problem358.InterceptEndpointExtension.exists_normalized_lipschitz_extension line 147

Source documentation

The normalization of an interior intercept path extends to both endpoints. The extension is globally measurable, hence can be used directly by the finite affine-potential time-integration interface.

theorem exists_normalized_lipschitz_extension
    {ι : Type*} [Fintype ι] (m : ι → ℝ) (c r : ι → ℝ → ℝ)
    {a b energy : ℝ} (hab : a < b) (hm : ∀ i, 0 < m i)
    (hderiv : ∀ i t, t ∈ Ioo a b → HasDerivAt (c i) (r i t) t)
    (henergy : ∀ t ∈ Ioo a b, (∑ i, m i * r i t ^ 2) ≤ energy)
    (hnormal : ∀ t ∈ Ioo a b, (∑ i, m i * c i t) = 0) :
    ∃ C : ι → ℝ → ℝ,
      (∀ i, LipschitzWith ⟨Real.sqrt (energy / m i), Real.sqrt_nonneg _⟩ (C i)) ∧
      (∀ i, EqOn (c i) (C i) (Ioo a b)) ∧
      (∀ i t, t ∈ Ioo a b → HasDerivAt (C i) (r i t) t) ∧
      (∀ t ∈ Icc a b, (∑ i, m i * C i t) = 0) ∧
      (∀ i, Measurable (C i)) := by
…

def OAI.Problem358.WeightedEndpointEnergy.weightedVector line 188
Source documentation
Encode the weighted coefficient norm in a Euclidean space.
```
def weightedVector (m z : ι → ℝ) : EuclideanSpace ℝ ι :=
…
```
theorem OAI.Problem358.WeightedEndpointEnergy.norm_weightedVector_sq line 191
theorem OAI.Problem358.WeightedEndpointEnergy.weightedVector_sub line 199
theorem OAI.Problem358.WeightedEndpointEnergy.hasDerivAt_weightedVector line 204

theorem OAI.Problem358.WeightedEndpointEnergy.weighted_path_lipschitzOn_Ioo line 215

Source documentation

The weighted coefficient path is Lipschitz with the square root of its aggregate energy bound, independently of the number and sizes of the masses.

theorem weighted_path_lipschitzOn_Ioo
    (m : ι → ℝ) (c r : ι → ℝ → ℝ) {a b energy : ℝ}
    (hm : ∀ i, 0 ≤ m i) (he : 0 ≤ energy)
    (hd : ∀ i t, t ∈ Ioo a b → HasDerivAt (c i) (r i t) t)
    (henergy : ∀ t ∈ Ioo a b, ∑ i, m i * r i t ^ 2 ≤ energy) :
    LipschitzOnWith ⟨Real.sqrt energy, Real.sqrt_nonneg _⟩
      (fun t => weightedVector m (fun i => c i t)) (Ioo a b) := by
…

Mentions: OAI.Problem358.WeightedEndpointEnergy.weightedVector

theorem OAI.Problem358.WeightedEndpointEnergy.weighted_path_lipschitzOn_Icc line 232

Source documentation

Continuity extends the mass-independent weighted Lipschitz estimate to the endpoints. Zero masses are allowed in this estimate.

theorem weighted_path_lipschitzOn_Icc
    (m : ι → ℝ) (c r : ι → ℝ → ℝ) {a b energy : ℝ}
    (hab : a < b) (hm : ∀ i, 0 ≤ m i) (he : 0 ≤ energy)
    (hc : ∀ i, ContinuousOn (c i) (Icc a b))
    (hd : ∀ i t, t ∈ Ioo a b → HasDerivAt (c i) (r i t) t)
    (henergy : ∀ t ∈ Ioo a b, ∑ i, m i * r i t ^ 2 ≤ energy) :
    LipschitzOnWith ⟨Real.sqrt energy, Real.sqrt_nonneg _⟩
      (fun t => weightedVector m (fun i => c i t)) (Icc a b) := by
…

Mentions: OAI.Problem358.WeightedEndpointEnergy.weightedVector

theorem OAI.Problem358.WeightedEndpointEnergy.weighted_displacement_sq_le line 250

Source documentation

Aggregate endpoint coefficient displacement inherits exactly the derivative energy constant; unlike coordinatewise summation there is no cardinality loss.

theorem weighted_displacement_sq_le
    (m : ι → ℝ) (c r : ι → ℝ → ℝ) {a b energy s t : ℝ}
    (hab : a < b) (hm : ∀ i, 0 ≤ m i) (he : 0 ≤ energy)
    (hc : ∀ i, ContinuousOn (c i) (Icc a b))
    (hd : ∀ i q, q ∈ Ioo a b → HasDerivAt (c i) (r i q) q)
    (henergy : ∀ q ∈ Ioo a b, ∑ i, m i * r i q ^ 2 ≤ energy)
    (hs : s ∈ Icc a b) (ht : t ∈ Icc a b) :
    ∑ i, m i * (c i t - c i s) ^ 2 ≤ energy * (t - s) ^ 2 := by
…