Coarse-graining support: Support.Book.Ch03.Theorems.CoarsePoincare.Infinity

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Section 3.1.1: Coarse Poincare infinity-depth estimates

This file contains the infinity-depth scalar algebra and series identities used by the public coarse Poincare theorem package.

theorem HCPolySupport.Book.Ch03.multiscaleDescendantWeight_sub_nat {d : ℕ} (Q : TriadicCube d) (s : ℝ) (j : ℕ) : Ch02.multiscaleDescendantWeight Q (Q.scale - ↑j) s = Real.rpow 3 (2 * s * ↑j)

theorem HCPolySupport.Book.Ch03.rpow_inv_half_eq_rpow_neg_half {x : ℝ} (hx : 0 ≤ x) : x⁻¹.rpow (1 / 2) = x.rpow (-(1 / 2))

theorem HCPolySupport.Book.Ch03.rpow_depth_weight_sqrt_cancel {s : ℝ} (j : ℕ) {L E : ℝ} (hL : 0 ≤ L) (hE : 0 ≤ E) : Real.rpow 3 (-s * ↑j) * √(Real.rpow 3 (2 * s * ↑j) * L * E) = L.rpow (1 / 2) * √E

theorem HCPolySupport.Book.Ch03.infinity_gradient_norm_le_of_cubeAverageEnergyControl {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffFamily d) (s : ℝ) (hs : 0 < s) (F : Vec d → Vec d) (energy : Vec d → ℝ) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (hdepthAverage : ∀ (n : ℕ), negativeBesovVectorDepthAverage Q F n ≤ Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑n) a * cubeAverage Q energy) : scaleNormalizedNegativeBesovVectorNorm Q s Ch02.MultiscaleExponent.infinity F ≤ poincareDiscountFactor s Ch02.MultiscaleExponent.infinity * poincareLowerEllipticityFactor Q a s Ch02.MultiscaleExponent.infinity * √(cubeAverage Q energy)

theorem HCPolySupport.Book.Ch03.infinity_flux_norm_le_of_cubeAverageEnergyControl {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffFamily d) (s : ℝ) (hs : 0 < s) (F : Vec d → Vec d) (energy : Vec d → ℝ) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (hdepthAverage : ∀ (n : ℕ), negativeBesovVectorDepthAverage Q F n ≤ Ch02.maxDescendantBMatrixNormAtScale Q (Q.scale - ↑n) a * cubeAverage Q energy) : scaleNormalizedNegativeBesovVectorNorm Q s Ch02.MultiscaleExponent.infinity F ≤ poincareDiscountFactor s Ch02.MultiscaleExponent.infinity * poincareUpperEllipticityFactor Q a s Ch02.MultiscaleExponent.infinity * √(cubeAverage Q energy)

theorem HCPolySupport.Book.Ch03.summable_public_sigmaStar_series {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffFamily d) {s q : ℝ} (hs : 0 < s) (hq : 0 < q) : Summable fun (n : ℕ) => Ch02.geometricWeight s q n * (Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2)

theorem HCPolySupport.Book.Ch03.summable_public_B_series {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffFamily d) {s q : ℝ} (hs : 0 < s) (hq : 0 < q) : Summable fun (n : ℕ) => Ch02.geometricWeight s q n * (Ch02.maxDescendantBMatrixNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2)

theorem HCPolySupport.Book.Ch03.tsum_public_sigmaStar_series_eq_lambdaSq {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) {s q : ℝ} (hs : 0 < s) (hq : 0 < q) : ∑' (n : ℕ), Ch02.geometricWeight s q n * (Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2) = (Ch02.lambdaSq Q s (Ch02.MultiscaleExponent.finite q) a).rpow (-q / 2)

theorem HCPolySupport.Book.Ch03.tsum_public_B_series_eq_LambdaSq {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) {s q : ℝ} (hs : 0 < s) (hq : 0 < q) : ∑' (n : ℕ), Ch02.geometricWeight s q n * (Ch02.maxDescendantBMatrixNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2) = (Ch02.LambdaSq Q s (Ch02.MultiscaleExponent.finite q) a).rpow (q / 2)