AffinePaths.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem358.finite_affine_path_L2_bound line 17

Source documentation

Quantitative time stability for a genuine finite affine maximum with fixed cell masses. Null ties, time regularity, square integrability, and the fundamental theorem are derived from the stated coefficient data rather than assumed for the potential.

theorem finite_affine_path_L2_bound
    {d : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι]
    [MeasurableSpace ι] [MeasurableSingletonClass ι]
    (K : Set (E d)) [IsFiniteMeasure (uniformMeasure K)]
    (y v : ι → ℝ → E d) (c r : ι → ℝ → ℝ)
    (active : ℝ × E d → ι) (m : ι → ℝ)
    {a b w κ : ℝ} {R A B : ℝ≥0}
    (hab : a < b) (hw : 0 ≤ w) (hκ : 0 ≤ κ)
    (hxR : ∀ᵐ x ∂uniformMeasure K, ‖x‖ ≤ R)
    (hy : ∀ i, Measurable (y i)) (hc : ∀ i, Measurable (c i))
    (hv : ∀ i, Measurable (v i)) (hr : ∀ i, Measurable (r i))
    (hactiveMeas : Measurable active)
…

theorem OAI.Problem358.FiniteAffine.abs_potential_sub_le_coefficients line 126
Source documentation
Uniform comparison of finite affine maxima, without any uniqueness of active indices or separation of the sites.
```
theorem abs_potential_sub_le_coefficients (y z : I → F) (c b : I → ℝ)
    {R : ℝ} (hR : 0 ≤ R) {x : F} (hx : ‖x‖ ≤ R) :
    |potential y c x - potential z b x| ≤
      R * ∑ i, ‖y i - z i‖ + ∑ i, |c i - b i| := by
…
```
Mentions: OAI.Problem358.FiniteAffine.potential

theorem OAI.Problem358.FiniteAffine.tendsto_integral_potential_sub_sq line 168

Source documentation

Coefficient convergence gives scalar L² convergence on every finite bounded source. Arbitrary filters are allowed, including both endpoint filters; repeated limiting sites cause no issue.

theorem tendsto_integral_potential_sub_sq
    {A : Type*} {l : Filter A} {y : A → I → F} {c : A → I → ℝ}
    {z : I → F} {b : I → ℝ} {R : ℝ} (hR : 0 ≤ R)
    (hx : ∀ᵐ x ∂μ, ‖x‖ ≤ R)
    (hy : ∀ i, Tendsto (fun t => y t i) l (𝓝 (z i)))
    (hc : ∀ i, Tendsto (fun t => c t i) l (𝓝 (b i))) :
    Tendsto (fun t => ∫ x, (potential (y t) (c t) x - potential z b x) ^ 2 ∂μ)
      l (𝓝 0) := by
…

Mentions: OAI.Problem358.FiniteAffine.potential

theorem OAI.Problem358.FiniteAffine.tendsto_sqrt_integral_potential_sub_sq line 202

Source documentation

Norm-form endpoint convergence of the finite affine potentials.

theorem tendsto_sqrt_integral_potential_sub_sq
    {A : Type*} {l : Filter A} {y : A → I → F} {c : A → I → ℝ}
    {z : I → F} {b : I → ℝ} {R : ℝ} (hR : 0 ≤ R)
    (hx : ∀ᵐ x ∂μ, ‖x‖ ≤ R)
    (hy : ∀ i, Tendsto (fun t => y t i) l (𝓝 (z i)))
    (hc : ∀ i, Tendsto (fun t => c t i) l (𝓝 (b i))) :
    Tendsto (fun t => Real.sqrt
      (∫ x, (potential (y t) (c t) x - potential z b x) ^ 2 ∂μ)) l (𝓝 0) := by
…

Mentions: OAI.Problem358.FiniteAffine.potential

theorem OAI.Problem358.FiniteAffine.sqrt_integral_sub_sq_eq_dist line 215

Source documentation

The scalar square-root energy is the genuine L² metric.

theorem sqrt_integral_sub_sq_eq_dist {f g : F → ℝ}
    (hf : MemLp f 2 μ) (hg : MemLp g 2 μ) :
    Real.sqrt (∫ x, (f x - g x) ^ 2 ∂μ) =
      dist (hf.toLp f) (hg.toLp g) := by
…

theorem OAI.Problem358.FiniteAffine.tendsto_sqrt_integral_pair_sub_sq line 226

Source documentation

L² convergence of both endpoints preserves their scalar L² distance.

theorem tendsto_sqrt_integral_pair_sub_sq
    {A : Type*} {l : Filter A} {u v : A → F → ℝ} {u₀ v₀ : F → ℝ}
    (hu : ∀ t, MemLp (u t) 2 μ) (hv : ∀ t, MemLp (v t) 2 μ)
    (hu₀ : MemLp u₀ 2 μ) (hv₀ : MemLp v₀ 2 μ)
    (hul : Tendsto (fun t => Real.sqrt (∫ x, (u t x - u₀ x) ^ 2 ∂μ)) l (𝓝 0))
    (hvl : Tendsto (fun t => Real.sqrt (∫ x, (v t x - v₀ x) ^ 2 ∂μ)) l (𝓝 0)) :
    Tendsto (fun t => Real.sqrt (∫ x, (u t x - v t x) ^ 2 ∂μ))
      l (𝓝 (Real.sqrt (∫ x, (u₀ x - v₀ x) ^ 2 ∂μ))) := by
…

theorem OAI.Problem358.FiniteAffine.memLp_potential_of_ae_norm_le line 245
Source documentation
Finite affine potentials are in L² on every finite bounded source.
```
theorem memLp_potential_of_ae_norm_le (y : I → F) (c : I → ℝ)
    {R : ℝ} (hR : 0 ≤ R) (hx : ∀ᵐ x ∂μ, ‖x‖ ≤ R) :
    MemLp (potential y c) 2 μ := by
…
```
Mentions: OAI.Problem358.FiniteAffine.potential

theorem OAI.Problem358.FiniteAffine.tendsto_sqrt_integral_potential_pair_sub_sq line 256

Source documentation

Endpoint coefficients alone suffice for continuity of the distance between two finite affine potentials.

theorem tendsto_sqrt_integral_potential_pair_sub_sq
    {A : Type*} {l : Filter A}
    {y z : A → I → F} {c b : A → I → ℝ}
    {y₀ z₀ : I → F} {c₀ b₀ : I → ℝ} {R : ℝ} (hR : 0 ≤ R)
    (hx : ∀ᵐ x ∂μ, ‖x‖ ≤ R)
    (hy : ∀ i, Tendsto (fun t => y t i) l (𝓝 (y₀ i)))
    (hc : ∀ i, Tendsto (fun t => c t i) l (𝓝 (c₀ i)))
    (hz : ∀ i, Tendsto (fun t => z t i) l (𝓝 (z₀ i)))
    (hb : ∀ i, Tendsto (fun t => b t i) l (𝓝 (b₀ i))) :
    Tendsto (fun t => Real.sqrt
      (∫ x, (potential (y t) (c t) x - potential (z t) (b t) x) ^ 2 ∂μ))
      l (𝓝 (Real.sqrt (∫ x, (potential y₀ c₀ x - potential z₀ b₀ x) ^ 2 ∂μ))) := by
…

Mentions: OAI.Problem358.FiniteAffine.potential

theorem OAI.Problem358.exists_uniform_norm_bound_of_weighted_energy line 290

Source documentation

Positive finite weights turn a uniform weighted square bound into a uniform coordinate norm bound. The bound is used only for local time regularity; it does not enter the final potential stability constant.

theorem exists_uniform_norm_bound_of_weighted_energy
    {ι P F : Type*} [Fintype ι] [NormedAddCommGroup F]
    (m : ι → ℝ) (f : ι → P → F) (S : Set P) {C : ℝ}
    (hm : ∀ i, 0 < m i)
    (henergy : ∀ q ∈ S, (∑ i, m i * ‖f i q‖ ^ 2) ≤ C) :
    ∃ A : ℝ≥0, ∀ i q, q ∈ S → ‖f i q‖ ≤ A := by
…

theorem OAI.Problem358.ParameterizedArgmax.exists_joint_measurable_affine_argmax_with_masses_on line 316

Source documentation

On a specified parameter set, pointwise prescribed-mass witnesses suffice for one globally measurable affine maximizing selector. No separation or mass condition is imposed outside that set.

theorem ParameterizedArgmax.exists_joint_measurable_affine_argmax_with_masses_on
    {P ι : Type*} [MeasurableSpace P] [MeasurableSpace ι]
    [Fintype ι] [Nonempty ι] {d : ℕ} (K : Set (E d)) (S : Set P)
    (y : P → ι → E d) (c m : P → ι → ℝ)
    (hy : ∀ i, Measurable (fun p => y p i))
    (hc : ∀ i, Measurable (fun p => c p i))
    (hinj : ∀ p ∈ S, Function.Injective (y p))
    (hex : ∀ p ∈ S, ∃ k : E d → ι,
      (∀ᵐ x ∂uniformMeasure K, ∀ i,
        ⟪x, y p i⟫_ℝ + c p i ≤ ⟪x, y p (k x)⟫_ℝ + c p (k x)) ∧
      ∀ i, (uniformMeasure K).real {x | k x = i} = m p i) :
    ∃ k : P × E d → ι, Measurable k ∧
…

theorem OAI.Problem358.finite_affine_path_L2_bound_of_positive_cell_masses line 356

Source documentation

Interior finite-potential stability directly from positive fixed masses and weighted energies. Joint selection and auxiliary coordinate derivative bounds are consequences, not extra hypotheses. In particular, sites may collide outside the integration interval.

theorem finite_affine_path_L2_bound_of_positive_cell_masses
    {d : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι]
    [MeasurableSpace ι] [MeasurableSingletonClass ι]
    (K : Set (E d)) [IsFiniteMeasure (uniformMeasure K)]
    (y v : ι → ℝ → E d) (c r : ι → ℝ → ℝ) (m : ι → ℝ)
    {a b w κ : ℝ} {R : ℝ≥0}
    (hab : a < b) (hw : 0 ≤ w) (hκ : 0 ≤ κ)
    (hm : ∀ i, 0 < m i)
    (hxR : ∀ᵐ x ∂uniformMeasure K, ‖x‖ ≤ R)
    (hy : ∀ i, Measurable (y i)) (hc : ∀ i, Measurable (c i))
    (hv : ∀ i, Measurable (v i)) (hr : ∀ i, Measurable (r i))
    (hdy : ∀ i q, q ∈ Icc a b → HasDerivAt (y i) (v i q) q)
…

theorem OAI.Problem358.finite_affine_path_endpoint_bound line 413

Source documentation

An interior time estimate for finite affine potentials passes to both endpoints using only continuity of the coefficients. Sites may collide at either endpoint.

theorem finite_affine_path_endpoint_bound
    {d : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι]
    (K : Set (E d)) [IsFiniteMeasure (uniformMeasure K)]
    (y : ι → ℝ → E d) (c : ι → ℝ → ℝ) {R L : ℝ}
    (hR : 0 ≤ R) (hL : 0 ≤ L)
    (hxR : ∀ᵐ x ∂uniformMeasure K, ‖x‖ ≤ R)
    (hy : ∀ i, Continuous (y i)) (hc : ∀ i, Continuous (c i))
    (hinterior : ∀ a b : ℝ, 0 < a → a < b → b < 1 →
      Real.sqrt (∫ x,
        (FiniteAffine.potential (fun i => y i b) (fun i => c i b) x -
         FiniteAffine.potential (fun i => y i a) (fun i => c i a) x) ^ 2
        ∂uniformMeasure K) ≤ L * (b - a)) :
…

Mentions: OAI.Problem358.FiniteAffine.potential

theorem OAI.Problem358.finite_affine_path_endpoint_integral_bound line 448

Source documentation

Squared form of the endpoint bound for use in gradient interpolation.

theorem finite_affine_path_endpoint_integral_bound
    {d : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι]
    (K : Set (E d)) [IsFiniteMeasure (uniformMeasure K)]
    (y : ι → ℝ → E d) (c : ι → ℝ → ℝ) {R L : ℝ}
    (hR : 0 ≤ R) (hL : 0 ≤ L)
    (hxR : ∀ᵐ x ∂uniformMeasure K, ‖x‖ ≤ R)
    (hy : ∀ i, Continuous (y i)) (hc : ∀ i, Continuous (c i))
    (hinterior : ∀ a b : ℝ, 0 < a → a < b → b < 1 →
      Real.sqrt (∫ x,
        (FiniteAffine.potential (fun i => y i b) (fun i => c i b) x -
         FiniteAffine.potential (fun i => y i a) (fun i => c i a) x) ^ 2
        ∂uniformMeasure K) ≤ L * (b - a)) :
…

Mentions: OAI.Problem358.FiniteAffine.potential

theorem OAI.Problem358.finite_affine_C1_path_endpoint_L2_bound line 470

Source documentation

A finite C¹ fixed-mass path on the open time interval has the full endpoint estimate. Derivatives need neither exist nor stay bounded near endpoints; continuity of the endpoint coefficients is sufficient.

theorem finite_affine_C1_path_endpoint_L2_bound
    {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)
    (hy : ∀ i, Continuous (y i)) (hc : ∀ i, Continuous (c i))
    (hv : ∀ i, ContinuousOn (v i) (Ioo 0 1))
    (hr : ∀ i, ContinuousOn (r i) (Ioo 0 1))
    (hactiveMeas : Measurable active)
…