MomentAlgebra.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem358.midpoint_energy_absorption line 12

Source documentation

The energy absorption step in the stationary-site moment estimate.

theorem midpoint_energy_absorption {A B R : ℝ}
    (hA : 0 ≤ A) (hB : 0 ≤ B)
    (h : A / 4 ≤ R ^ 2 * B / 8 + R / 2 * Real.sqrt (A * B)) :
    A ≤ 5 * R ^ 2 * B := by
…

theorem OAI.Problem358.nearby_mass_square_bound line 24
Source documentation
Uniform comparisons of nearby cell masses, in the normalization used in the finite-difference estimate.
```
theorem nearby_mass_square_bound {M α γ : ℝ}
    (hM : 0 < M) (hα : 0 ≤ α) (hαM : α ≤ 2 * M)
    (hγM : M / 2 ≤ γ) : α ^ 2 / M ≤ 8 * γ := by
…
```

theorem OAI.Problem358.nearby_mass_reciprocal_bound line 32

Source documentation

The reciprocal comparison for nearby cell masses.

theorem nearby_mass_reciprocal_bound {M γ δ : ℝ}
    (hM : 0 < M) (hγM : M / 2 ≤ γ) :
    δ ^ 2 / γ ≤ 2 * (δ ^ 2 / M) := by
…

theorem OAI.Problem358.stationary_moment_finite_difference line 46

Source documentation

A finite-difference moment estimate with a constant independent of the number of cells or the smallest cell mass. The geometric input is the midpoint energy estimate and the elementary bound on each moment change.

theorem stationary_moment_finite_difference
    {ι V : Type*} [Fintype ι] [SeminormedAddCommGroup V]
    (M α γ δ D : ι → ℝ) (Δ : ι → V) (R : ℝ)
    (hM : ∀ i, 0 < M i) (hα : ∀ i, 0 ≤ α i)
    (hαM : ∀ i, α i ≤ 2 * M i)
    (hγM : ∀ i, M i / 2 ≤ γ i)
    (hD : ∀ i, 0 ≤ D i) (hR : 0 ≤ R)
    (hΔ : ∀ i, ‖Δ i‖ ≤ R * |δ i| + α i * Real.sqrt (D i))
    (henergy : (∑ i, γ i * D i) ≤
      5 * R ^ 2 * (∑ i, δ i ^ 2 / γ i)) :
    (∑ i, ‖Δ i‖ ^ 2 / M i) ≤
      162 * R ^ 2 * (∑ i, δ i ^ 2 / M i) := by
…

theorem OAI.Problem358.eventually_nearby_mass_bounds line 101

Source documentation

Positive limiting cell masses give all nearby-mass comparisons simultaneously, with no uniform lower bound on the finite configuration.

theorem eventually_nearby_mass_bounds
    {ι A : Type*} [Finite ι] {l : Filter A}
    (M : ι → ℝ) (α β : A → ι → ℝ)
    (hM : ∀ i, 0 < M i)
    (hα : ∀ i, Filter.Tendsto (fun a => α a i) l (nhds (M i)))
    (hβ : ∀ i, Filter.Tendsto (fun a => β a i) l (nhds (M i))) :
    ∀ᶠ a in l, ∀ i, 0 < α a i ∧ 0 < β a i ∧
      α a i ≤ 2 * M i ∧ M i / 2 ≤ Real.sqrt (α a i * β a i) := by
…

theorem OAI.Problem358.eventually_stationary_moment_finite_difference line 123

Source documentation

The raw geometric moment inputs imply the uniform finite-difference estimate eventually, using continuity of the actual two endpoint masses.

theorem eventually_stationary_moment_finite_difference
    {ι V A : Type*} [Fintype ι] [SeminormedAddCommGroup V] {l : Filter A}
    (M : ι → ℝ) (α β δ D : A → ι → ℝ) (Δ : A → ι → V) (R : ℝ)
    (hM : ∀ i, 0 < M i) (hR : 0 ≤ R)
    (hα : ∀ i, Filter.Tendsto (fun a => α a i) l (nhds (M i)))
    (hβ : ∀ i, Filter.Tendsto (fun a => β a i) l (nhds (M i)))
    (hD : ∀ᶠ a in l, ∀ i, 0 ≤ D a i)
    (hΔ : ∀ᶠ a in l, ∀ i,
      ‖Δ a i‖ ≤ R * |δ a i| + α a i * Real.sqrt (D a i))
    (henergy : ∀ᶠ a in l,
      (∑ i, Real.sqrt (α a i * β a i) * D a i) ≤
      5 * R ^ 2 * (∑ i, δ a i ^ 2 / Real.sqrt (α a i * β a i))) :
…

theorem OAI.Problem358.weighted_moment_energy_smul line 145

Source documentation

Weighted squared norm energies scale quadratically.

theorem weighted_moment_energy_smul
    {ι V : Type*} [Fintype ι] [SeminormedAddCommGroup V] [NormedSpace ℝ V]
    (M : ι → ℝ) (B : ι → V) (c : ℝ) :
    (∑ i, ‖c • B i‖ ^ 2 / M i) = c ^ 2 * (∑ i, ‖B i‖ ^ 2 / M i) := by
…

theorem OAI.Problem358.stationary_moment_limit line 155

Source documentation

The finite moment inequality passes to derivative limits. The arbitrary scale c is typically (2*s)⁻¹; stating the argument for any filter also permits one-sided finite differences and sequences.

theorem stationary_moment_limit
    {ι V A : Type*} [Fintype ι] [SeminormedAddCommGroup V] [NormedSpace ℝ V]
    {l : Filter A} [l.NeBot]
    (M : ι → ℝ) (B : A → ι → V) (m : A → ι → ℝ)
    (c : A → ℝ) (dB : ι → V) (dm : ι → ℝ) (C : ℝ)
    (hB : ∀ i, Filter.Tendsto (fun a => c a • B a i) l (nhds (dB i)))
    (hm : ∀ i, Filter.Tendsto (fun a => c a * m a i) l (nhds (dm i)))
    (hbound : ∀ᶠ a in l, (∑ i, ‖B a i‖ ^ 2 / M i) ≤
      C * (∑ i, m a i ^ 2 / M i)) :
    (∑ i, ‖dB i‖ ^ 2 / M i) ≤ C * (∑ i, dm i ^ 2 / M i) := by
…

theorem OAI.Problem358.stationary_moment_limit_of_continuous_masses line 185

Source documentation

The stationary-site derivative estimate from continuous endpoint masses, the geometric energy input, and genuine limits of the scaled differences.

theorem stationary_moment_limit_of_continuous_masses
    {ι V A : Type*} [Fintype ι] [SeminormedAddCommGroup V] [NormedSpace ℝ V]
    {l : Filter A} [l.NeBot]
    (M : ι → ℝ) (α β δ D : A → ι → ℝ) (Δ : A → ι → V) (R : ℝ)
    (c : A → ℝ) (dB : ι → V) (dm : ι → ℝ)
    (hM : ∀ i, 0 < M i) (hR : 0 ≤ R)
    (hα : ∀ i, Filter.Tendsto (fun a => α a i) l (nhds (M i)))
    (hβ : ∀ i, Filter.Tendsto (fun a => β a i) l (nhds (M i)))
    (hD : ∀ᶠ a in l, ∀ i, 0 ≤ D a i)
    (hΔ : ∀ᶠ a in l, ∀ i,
      ‖Δ a i‖ ≤ R * |δ a i| + α a i * Real.sqrt (D a i))
    (henergy : ∀ᶠ a in l,
…

theorem OAI.Problem358.mass_geometric_mean_gap line 218

Source documentation

Quantitative arithmetic--geometric mean gap for two positive cell masses.

theorem mass_geometric_mean_gap {a b : ℝ} (ha : 0 < a) (hb : 0 < b) :
    (a + b) / 2 - Real.sqrt (a * b) ≤
      (a - b) ^ 2 / (8 * Real.sqrt (a * b)) := by
…

theorem OAI.Problem358.moment_weighted_cauchy line 227

Source documentation

Weighted Cauchy--Schwarz in precisely the variables used by the cell argument.

theorem moment_weighted_cauchy {ι : Type*} [Fintype ι]
    {δ γ D : ι → ℝ} (hγ : ∀ i, 0 < γ i) (hD : ∀ i, 0 ≤ D i) :
    (∑ i, |δ i| * Real.sqrt (D i)) ≤
      Real.sqrt ((∑ i, γ i * D i) * (∑ i, δ i ^ 2 / γ i)) := by
…

theorem OAI.Problem358.tendsto_symmetric_moment_quotient line 250

Source documentation

Symmetric moment differences converge to the negative derivative.

theorem tendsto_symmetric_moment_quotient {V : Type*}
    [NormedAddCommGroup V] [NormedSpace ℝ V]
    {f : ℝ → V} {v : V} (hf : HasDerivAt f v 0) :
    Filter.Tendsto (fun s : ℝ => (2 * s)⁻¹ • (f (-s) - f s))
      (𝓝[>] 0) (𝓝 (-v)) := by
…

theorem OAI.Problem358.moment_derivative_bound line 271

Source documentation

Passing a uniform symmetric finite-difference estimate to cell derivatives. The geometric construction supplies hfinite; this lemma performs the limit step.

theorem moment_derivative_bound {ι V : Type*} [Fintype ι]
    [NormedAddCommGroup V] [NormedSpace ℝ V]
    {B : ι → ℝ → V} {m : ι → ℝ → ℝ}
    {dB : ι → V} {dm M : ι → ℝ} {C : ℝ}
    (hB : ∀ i, HasDerivAt (B i) (dB i) 0)
    (hm : ∀ i, HasDerivAt (m i) (dm i) 0)
    (hfinite : ∀ᶠ s : ℝ in 𝓝[>] 0,
      (∑ i, ‖B i (-s) - B i s‖ ^ 2 / M i) ≤
        C * ∑ i, (m i (-s) - m i s) ^ 2 / M i) :
    (∑ i, ‖dB i‖ ^ 2 / M i) ≤ C * ∑ i, dm i ^ 2 / M i := by
…

theorem OAI.Problem358.MomentCouplingBounds.integral_norm_le_sqrt_integral_sq_norm line 315
Source documentation
The elementary probability-space L1/L2 comparison for a norm.
```
theorem integral_norm_le_sqrt_integral_sq_norm {f : A → F} (hf : MemLp f 2 μ) :
    (∫ x, ‖f x‖ ∂μ) ≤ Real.sqrt (∫ x, ‖f x‖ ^ 2 ∂μ) := by
…
```

theorem OAI.Problem358.MomentCouplingBounds.norm_integral_sub_le_sqrt line 323

Source documentation

A coupling's quadratic displacement bounds the displacement of its barycentres.

theorem norm_integral_sub_le_sqrt [NormedSpace ℝ F] {X Z : A → F}
    (hX : MemLp X 2 μ) (hZ : MemLp Z 2 μ) :
    ‖(∫ x, X x ∂μ) - ∫ x, Z x ∂μ‖ ≤
      Real.sqrt (∫ x, ‖X x - Z x‖ ^ 2 ∂μ) := by
…

theorem OAI.Problem358.MomentCouplingBounds.abs_sq_norm_sub_le line 332

Source documentation

Squared norms are 2R-Lipschitz on a ball of radius R.

theorem abs_sq_norm_sub_le {R : ℝ} {x z : F} (hx : ‖x‖ ≤ R) (hz : ‖z‖ ≤ R) :
    |‖x‖ ^ 2 - ‖z‖ ^ 2| ≤ 2 * R * ‖x - z‖ := by
…

theorem OAI.Problem358.MomentCouplingBounds.quadratic_potential_expectation_sub_le line 345

Source documentation

The quadratic concave potential used in the midpoint argument has controlled expectation difference under a bounded coupling.

theorem quadratic_potential_expectation_sub_le {R : ℝ} (hR : 0 ≤ R)
    {X Z : A → F} (hX : MemLp X 2 μ) (hZ : MemLp Z 2 μ)
    (hXR : ∀ᵐ x ∂μ, ‖X x‖ ≤ R) (hZR : ∀ᵐ x ∂μ, ‖Z x‖ ≤ R) :
    |(∫ x, R ^ 2 - ‖X x‖ ^ 2 ∂μ) - (∫ x, R ^ 2 - ‖Z x‖ ^ 2 ∂μ)| ≤
      2 * R * Real.sqrt (∫ x, ‖X x - Z x‖ ^ 2 ∂μ) := by
…

theorem OAI.Problem358.MomentCouplingBounds.norm_integral_le_of_ae_norm_le line 377

Source documentation

The expectation of a bounded random vector lies in the same norm ball.

theorem norm_integral_le_of_ae_norm_le [NormedSpace ℝ F] {X : A → F} {R : ℝ}
    (hX : Integrable X μ) (hXR : ∀ᵐ x ∂μ, ‖X x‖ ≤ R) :
    ‖∫ x, X x ∂μ‖ ≤ R := by
…

theorem OAI.Problem358.MomentCouplingBounds.weighted_barycentre_sub_le line 386

Source documentation

The unnormalized cell-moment difference estimate in the stationary-site proof.

theorem weighted_barycentre_sub_le [NormedSpace ℝ F] {X Z : A → F}
    (hX : MemLp X 2 μ) (hZ : MemLp Z 2 μ) {R α β : ℝ}
    (hα : 0 ≤ α) (hZR : ∀ᵐ x ∂μ, ‖Z x‖ ≤ R) :
    ‖α • (∫ x, X x ∂μ) - β • (∫ x, Z x ∂μ)‖ ≤
      R * |α - β| + α * Real.sqrt (∫ x, ‖X x - Z x‖ ^ 2 ∂μ) := by
…

def OAI.Problem358.MidpointEnergy.quadraticPotential line 413
Source documentation
The concave quadratic used in the midpoint argument.
```
def quadraticPotential (R : ℝ) (x : F) : ℝ := R ^ 2 - ‖x‖ ^ 2
```
lemma OAI.Problem358.MidpointEnergy.quadraticPotential_midpoint line 415
lemma OAI.Problem358.MidpointEnergy.quadraticPotential_nonneg line 424
lemma OAI.Problem358.MidpointEnergy.quadraticPotential_le line 429

theorem OAI.Problem358.MidpointEnergy.integral_quadraticPotential_midpoint line 435

Source documentation

The integrated parallelogram identity gives the exact midpoint energy gain.

theorem integral_quadraticPotential_midpoint (R : ℝ) {X Z : A → F}
    (hX : MemLp X 2 μ) (hZ : MemLp Z 2 μ) :
    (∫ x, quadraticPotential R ((1 / 2 : ℝ) • (X x + Z x)) ∂μ) =
      ((∫ x, quadraticPotential R (X x) ∂μ) +
        (∫ x, quadraticPotential R (Z x) ∂μ)) / 2 +
      (∫ x, ‖X x - Z x‖ ^ 2 ∂μ) / 4 := by
…

Mentions: OAI.Problem358.MidpointEnergy.quadraticPotential

theorem OAI.Problem358.MidpointEnergy.integrable_quadraticPotential_of_ae_bound line 458
Source documentation
A bounded-support measure integrates the nonnegative quadratic potential.
```
theorem integrable_quadraticPotential_of_ae_bound {ρ : Measure F} [IsFiniteMeasure ρ]
    {R : ℝ} (hρ : ∀ᵐ x ∂ρ, ‖x‖ ≤ R) : Integrable (quadraticPotential R) ρ := by
…
```
Mentions: OAI.Problem358.MidpointEnergy.quadraticPotential

theorem OAI.Problem358.MidpointEnergy.scaled_midpoint_energy_le line 468

Source documentation

Cellwise measure domination gives the midpoint energy inequality. The geometric existence of the dominated coupling is an explicit hypothesis.

theorem scaled_midpoint_energy_le {ρ : Measure F} [IsFiniteMeasure ρ]
    {R γ : ℝ} (hγ : 0 ≤ γ) {X Z : A → F}
    (hX : MemLp X 2 μ) (hZ : MemLp Z 2 μ)
    (hρ : ∀ᵐ x ∂ρ, ‖x‖ ≤ R)
    (hdom : ENNReal.ofReal γ •
      Measure.map (fun x => (1 / 2 : ℝ) • (X x + Z x)) μ ≤ ρ) :
    γ * (((∫ x, quadraticPotential R (X x) ∂μ) +
      (∫ x, quadraticPotential R (Z x) ∂μ)) / 2 +
      (∫ x, ‖X x - Z x‖ ^ 2 ∂μ) / 4) ≤
      ∫ x, quadraticPotential R x ∂ρ := by
…