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

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

Section 3.1.1: Coarse Poincare finite-depth estimates

This file contains the finite-depth scalar algebra and gradient/flux estimates used by the public coarse Poincare theorem package.

theorem HCPolySupport.Book.Ch03.rpow_inv_geometricDiscount_mul_geometricWeight {s q : ℝ} (hs : 0 < s) (hq : 0 < q) (j : ℕ) : Real.rpow 3 (-s * ↑j * q) = (Ch02.geometricDiscount s q)⁻¹ * Ch02.geometricWeight s q j

theorem HCPolySupport.Book.Ch03.rpow_finite_gradient_rhs {disc L E q : ℝ} (hdisc : 0 < disc) (hL : 0 ≤ L) (hE : 0 ≤ E) (hq : 0 < q) : (disc⁻¹ * L.rpow (-q / 2) * E.rpow (q / 2)).rpow (1 / q) = disc.rpow (-(1 / q)) * L.rpow (-(1 / 2)) * √E

theorem HCPolySupport.Book.Ch03.rpow_finite_flux_rhs {disc L E q : ℝ} (hdisc : 0 < disc) (hL : 0 ≤ L) (hE : 0 ≤ E) (hq : 0 < q) : (disc⁻¹ * L.rpow (q / 2) * E.rpow (q / 2)).rpow (1 / q) = disc.rpow (-(1 / q)) * L.rpow (1 / 2) * √E

theorem HCPolySupport.Book.Ch03.finite_gradient_norm_le_of_cubeAverageEnergyControl {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (s q : ℝ) (hs : 0 < s) (hq : 1 ≤ q) (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) (hsum : Summable fun (n : ℕ) => Ch02.geometricWeight s q n * (Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2)) (htsum : ∑' (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)) : scaleNormalizedNegativeBesovVectorNorm Q s (Ch02.MultiscaleExponent.finite q) F ≤ poincareDiscountFactor s (Ch02.MultiscaleExponent.finite q) * poincareLowerEllipticityFactor Q a s (Ch02.MultiscaleExponent.finite q) * √(cubeAverage Q energy)

theorem HCPolySupport.Book.Ch03.finite_flux_norm_le_of_cubeAverageEnergyControl {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (s q : ℝ) (hs : 0 < s) (hq : 1 ≤ q) (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) (hsum : Summable fun (n : ℕ) => Ch02.geometricWeight s q n * (Ch02.maxDescendantBMatrixNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2)) (htsum : ∑' (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)) : scaleNormalizedNegativeBesovVectorNorm Q s (Ch02.MultiscaleExponent.finite q) F ≤ poincareDiscountFactor s (Ch02.MultiscaleExponent.finite q) * poincareUpperEllipticityFactor Q a s (Ch02.MultiscaleExponent.finite q) * √(cubeAverage Q energy)