Bounds

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Local block energy: the bulk and cutoff estimates

Pointwise upper bounds on the bulk and cutoff densities of the test identity, absorbed against the energy density, following e.local.block.bulk and e.local.block.cutoff. Integrating gives the centered energy bound (e.local.block.centered.energy), the analytic core of T1.

• bulk: bulk x ≤ 5M²·η² + ⅛·𝓔-density;
• cutoff: cutoff x ≤ 5M²·η² + ⅟₁₆·𝓔-density + 67Θ·K∞²·|∇η|² (a.e.),

where M² = Θ|p|² + |q|². No EuclideanSpace.

Elementary scalar helpers

theorem HCPolySupport.abs_vecDot_le_sqrt_mul_sqrt {d : ℕ} (x y : Vec d) : |vecDot x y| ≤ √(vecNormSq x) * √(vecNormSq y)

Cauchy–Schwarz for the dot product in square-root form.

theorem HCPolySupport.mul_le_half_sq_add_half_sq (a b : ℝ) : a * b ≤ a ^ 2 / 2 + b ^ 2 / 2

a·b ≤ ½a² + ½b².

theorem HCPolySupport.amgm_of_sq_le {x c1 c2 : ℝ} (hx : 0 ≤ x) (hc1 : 0 ≤ c1) (hc2 : 0 ≤ c2) (hsq : x ^ 2 ≤ 4 * c1 * c2) : x ≤ c1 + c2

AM–GM from a squared bound: if x² ≤ 4c₁c₂ with x, c₁, c₂ ≥ 0 then x ≤ c₁ + c₂.

theorem HCPolySupport.amgm_term {K D nX nG A B : ℝ} (hK : 0 ≤ K) (hCS : D ^ 2 ≤ nX * nG) (hA : 0 ≤ A) (hB : 0 ≤ B) (hkey : K ^ 2 * (nX * nG) ≤ 4 * A * B) : K * |D| ≤ A + B

Cauchy–Schwarz + AM–GM packaged: from a dot-product Cauchy–Schwarz bound and a matching product bound, K·|D| ≤ A + B.

theorem HCPolySupport.cutoff_amgm_dot {d : ℕ} {K ηx N Q A B : ℝ} {X gS : Vec d} (hK : 0 ≤ K) (hgSN : vecNormSq gS = 4 * ηx ^ 2 * N) (hnX : vecNormSq X ≤ Q) (hA : 0 ≤ A) (hB : 0 ≤ B) (hfac : 0 ≤ 4 * K ^ 2 * ηx ^ 2 * N) (hkey : 4 * K ^ 2 * ηx ^ 2 * N * Q ≤ 4 * A * B) : K * |vecDot X gS| ≤ A + B

A single cutoff dot-product term: Cauchy–Schwarz against ∇(η²) plus AM–GM. |∇(η²)|² = 4η²N, |X|² ≤ Q, and 4K²η²N·Q = 4AB give K·|X·∇(η²)| ≤ A + B.

theorem HCPolySupport.cutoff_abs_split {uu uus K t1 t2 t3 t4 t5 : ℝ} (hK : 0 ≤ K) (huu : |uu| ≤ K) (huus : |uus| ≤ K) : uu * (t1 - t2 - 1 / 2 * t3) - uus * (t4 + 1 / 2 * t5) ≤ K * |t1| + K * |t2| + 1 / 2 * (K * |t3|) + K * |t4| + 1 / 2 * (K * |t5|)

The absolute-value decomposition of the cutoff density into five scalar terms, each dominated by K = K∞.

The bulk estimate

theorem HCPolySupport.bulkIntegrand_le {d : ℕ} {m : ℤ} {a : CoeffField d} {Θ : ℝ} {v vstar : H1Function (openCubeSet (originCube d m))} {P : BlockVec d} {η : Vec d → ℝ} (hEllO : IsEllipticFieldOn 1 Θ (openCubeSet (originCube d m)) a) {x : Vec d} (hx : x ∈ openCubeSet (originCube d m)) : bulkIntegrand a v vstar P η x ≤ 5 * (Θ * vecNormSq P.1 + vecNormSq P.2) * sqCutoff η x + 1 / 8 * energyIntegrand a v vstar P η x

Bulk density bound. For x ∈ U, bulk x ≤ 5M²·η²(x) + ⅛·(energy density)(x).

The cutoff estimate

theorem HCPolySupport.cutoffIntegrand_le {d : ℕ} {m : ℤ} {a : CoeffField d} {Θ : ℝ} {v vstar : H1Function (openCubeSet (originCube d m))} {P : BlockVec d} {η : Vec d → ℝ} {c Kinf : ℝ} (hEllO : IsEllipticFieldOn 1 Θ (openCubeSet (originCube d m)) a) (hη : ContDiff ℝ (↑⊤) η) {x : Vec d} (hx : x ∈ openCubeSet (originCube d m)) (hKv : |(centeredPotential m v P.1 c).toFun x| ≤ Kinf) (hKvs : |(centeredPotential m vstar P.1 (-c)).toFun x| ≤ Kinf) : cutoffIntegrand a v vstar P c η x ≤ 1 / 16 * energyIntegrand a v vstar P η x + 2 * (Θ * vecNormSq P.1 + vecNormSq P.2) * sqCutoff η x + 67 * Θ * Kinf ^ 2 * vecNormSq fun (i : Fin d) => (fderiv ℝ η x) (basisVec i)

Cutoff density bound (a.e.). For x ∈ U with |u|, |u*| ≤ K∞, requiring no range condition on the cutoff, cutoff x ≤ ⅟₁₆·(energy density)(x) + 2M²·η²(x) + 67Θ·K∞²·|∇η(x)|².