Flux.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Weighted finite-dimensional estimates for moving affine cells

These lemmas isolate the algebraic part of the moment and intercept-speed estimates. They make no assertion about existence or differentiability of cells.

theorem OAI.Problem358.weighted_inner_sum_sq_le line 23

Source documentation

Weighted Cauchy--Schwarz, in the form needed by the cell moment estimate.

theorem weighted_inner_sum_sq_le (s : Finset ι) (m : ι → ℝ)
    (v B : ι → F) (hm : ∀ i ∈ s, 0 < m i) :
    (∑ i ∈ s, inner ℝ (v i) (B i)) ^ 2 ≤
      (∑ i ∈ s, m i * ‖v i‖ ^ 2) *
        (∑ i ∈ s, ‖B i‖ ^ 2 / m i) := by
…

theorem OAI.Problem358.energy_le_of_sq_le_mul line 42

Source documentation

The energy cancellation step, including the zero-energy case.

theorem energy_le_of_sq_le_mul {energy bound : ℝ} (he : 0 ≤ energy) (hb : 0 ≤ bound)
    (h : energy ^ 2 ≤ bound * energy) : energy ≤ bound := by
…

theorem OAI.Problem358.intercept_energy_le line 52

Source documentation

Algebraic intercept-energy estimate from a moment estimate and cell duality. The geometric work supplies hdual and hmoment; no inverse bound on a Laplacian is used here.

theorem intercept_energy_le (s : Finset ι) (m r : ι → ℝ) (v B : ι → F)
    {k w : ℝ} (hm : ∀ i ∈ s, 0 < m i) (hk : 0 ≤ k)
    (hspeed : (∑ i ∈ s, m i * ‖v i‖ ^ 2) ≤ w ^ 2)
    (hdual : (∑ i ∈ s, m i * r i ^ 2) =
      -(∑ i ∈ s, inner ℝ (v i) (B i)))
    (hmoment : (∑ i ∈ s, ‖B i‖ ^ 2 / m i) ≤
      k * (∑ i ∈ s, m i * r i ^ 2)) :
    (∑ i ∈ s, m i * r i ^ 2) ≤ k * w ^ 2 := by
…

theorem OAI.Problem358.intercept_speed_le line 77

Source documentation

Square-root form of the intercept-speed estimate.

theorem intercept_speed_le (s : Finset ι) (m r : ι → ℝ) (v B : ι → F)
    {k w : ℝ} (hm : ∀ i ∈ s, 0 < m i) (hk : 0 ≤ k) (hw : 0 ≤ w)
    (hspeed : (∑ i ∈ s, m i * ‖v i‖ ^ 2) ≤ w ^ 2)
    (hdual : (∑ i ∈ s, m i * r i ^ 2) =
      -(∑ i ∈ s, inner ℝ (v i) (B i)))
    (hmoment : (∑ i ∈ s, ‖B i‖ ^ 2 / m i) ≤
      k * (∑ i ∈ s, m i * r i ^ 2)) :
    Real.sqrt (∑ i ∈ s, m i * r i ^ 2) ≤ Real.sqrt k * w := by
…

theorem OAI.Problem358.symmetric_flux_pairing line 92

Source documentation

Symmetry of the vector-valued face coefficients identifies the adjoint of site motion with the stationary-site moment derivative.

theorem symmetric_flux_pairing [Fintype ι] (q : ι → ℝ) (v : ι → F)
    (b : ι → ι → F) (hb : ∀ i j, b i j = b j i) :
    (∑ i, q i * ∑ j, inner ℝ (b i j) (v i - v j)) =
      ∑ i, inner ℝ (v i) (∑ j, (q i - q j) • b i j) := by
…

theorem OAI.Problem358.symmetric_mass_pairing line 113

Source documentation

Symmetry of scalar face coefficients gives the mass pairing identity.

theorem symmetric_mass_pairing [Fintype ι] (q r : ι → ℝ)
    (g : ι → ι → ℝ) (hg : ∀ i j, g i j = g j i) :
    (∑ i, q i * ∑ j, g i j * (r i - r j)) =
      ∑ i, r i * ∑ j, g i j * (q i - q j) := by
…

theorem OAI.Problem358.fixed_mass_flux_duality line 122

Source documentation

The finite-cell duality identity follows solely from symmetric face coefficients and the differentiated fixed-mass constraints.

theorem fixed_mass_flux_duality [Fintype ι] (q r : ι → ℝ) (v : ι → F)
    (g : ι → ι → ℝ) (b : ι → ι → F)
    (hg : ∀ i j, g i j = g j i) (hb : ∀ i j, b i j = b j i)
    (hfixed : ∀ i, (∑ j, g i j * (r i - r j)) +
      (∑ j, inner ℝ (b i j) (v i - v j)) = 0) :
    (∑ i, r i * ∑ j, g i j * (q i - q j)) =
      -(∑ i, inner ℝ (v i) (∑ j, (q i - q j) • b i j)) := by
…

theorem OAI.Problem358.weighted_abs_sqrt_sum_le line 141

Source documentation

Weighted Cauchy--Schwarz for the mass-displacement mixed term.

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

theorem OAI.Problem358.midpoint_displacement_energy_le line 159

Source documentation

Young's inequality absorbs the mixed square-root term in the stationary cell displacement estimate.

theorem midpoint_displacement_energy_le {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.geometric_mean_gap_bounds line 172

Source documentation

Elementary arithmetic/geometric mean gap bound without square-root normalization: the positive geometric mean can be supplied by its square.

theorem geometric_mean_gap_bounds {α β γ : ℝ} (hα : 0 ≤ α) (hβ : 0 ≤ β)
    (hγ : 0 < γ) (hγsq : γ ^ 2 = α * β) :
    0 ≤ (α + β) / 2 - γ ∧
      (α + β) / 2 - γ ≤ (α - β) ^ 2 / (8 * γ) := by
…

theorem OAI.Problem358.midpoint_cell_energy_balance line 182

Source documentation

The contribution of one cell to the aggregate midpoint energy balance.

theorem midpoint_cell_energy_balance {α β γ Am Ap D R : ℝ}
    (hα : 0 ≤ α) (hβ : 0 ≤ β) (hγ : 0 < γ) (hγsq : γ ^ 2 = α * β)
    (hAm : Am ≤ R ^ 2) (hAp : Ap ≤ R ^ 2)
    (hdiff : |Am - Ap| ≤ 2 * R * Real.sqrt D) :
    (α * Am + β * Ap) / 2 - γ * ((Am + Ap) / 2) ≤
      R ^ 2 * ((α - β) ^ 2 / γ) / 8 +
        R / 2 * (|α - β| * Real.sqrt D) := by
…

theorem OAI.Problem358.midpoint_aggregate_transport line 211

Source documentation

Aggregate midpoint domination and cellwise moment-control bounds imply the transport-energy estimate used in the uniform 162 moment bound.

theorem midpoint_aggregate_transport {ι : Type*} (s : Finset ι)
    (α β γ D Am Ap : ι → ℝ) {R : ℝ}
    (hα : ∀ i ∈ s, 0 ≤ α i) (hβ : ∀ i ∈ s, 0 ≤ β i)
    (hγ : ∀ i ∈ s, 0 < γ i) (hγsq : ∀ i ∈ s, γ i ^ 2 = α i * β i)
    (hD : ∀ i ∈ s, 0 ≤ D i) (hR : 0 ≤ R)
    (hAm : ∀ i ∈ s, Am i ≤ R ^ 2) (hAp : ∀ i ∈ s, Ap i ≤ R ^ 2)
    (hdiff : ∀ i ∈ s, |Am i - Ap i| ≤ 2 * R * Real.sqrt (D i))
    (hdom : (∑ i ∈ s, γ i * ((Am i + Ap i) / 2 + D i / 4)) ≤
      ∑ i ∈ s, (α i * Am i + β i * Ap i) / 2) :
    (∑ i ∈ s, γ i * D i) ≤
      5 * R ^ 2 * ∑ i ∈ s, (α i - β i) ^ 2 / γ i := by
…