Scalar #
Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.
Scalar block variance (e.scalar.block.variance) #
Assembly of the scalar estimate: for any origin cube 𝒰_m and block
vector P = (p, q),
Var[P · 𝐀(𝒰_m) P] ≤ C_d·(Θ|p|² + |q|²)²·min{1, Θ²·3^{-β_d·m}},
β_d = (d-2)/(d-1).
The three ingredients, each with a uniform dimensional constant:
fixed_phase_variance_uniform—Var[F_σ] ≤ C_fp·Θ³(ℓ/3^m)^{d-2}·Msq²;exists_gridPhase_meanSq_le_uniform— a grid phaseσwith∫|F_σ − F|² ≤ C_av·Θ·ℓ⁻¹·Msq²;- the deterministic a.s. bound
0 ≤ F ≤ 2·Msq(t.coarse.block.ellipticity).
Step (i) is the L²-projection split var_le_two_integral_add_two_var; step (ii)
combines the two errors at a free width ℓ ∈ [4, 3^m]; step (iii) is the rpow
optimization scalar_opt. The constant is fixed before the field quantifiers.
theorem
HCPolySupport.scalar_block_variance
{d : ℕ}
[NeZero d]
(hd : 3 ≤ d)
:
∃ (Cd : ℝ),
0 ≤ Cd ∧ ∀ {m : ℤ},
0 ≤ m →
∀ {Θ : ℝ},
1 ≤ Θ →
∀ {L : Book.Ch04.RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure L],
Book.Ch04.RestrictionLawCarrier L →
IsRestrictionUnitRangeDependentR L →
ThetaEllipticLaw Θ L →
∀ (P : BlockVec d),
ProbabilityTheory.variance
(fun (a : RegCoeffField d) =>
blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d m)) a.toFun) P))
L ≤ Cd * (Θ * vecNormSq P.1 + vecNormSq P.2) ^ 2 * min 1 (Θ ^ 2 * (3 ^ m) ^ (-(↑d - 2) / (↑d - 1)))
Scalar block variance. Dimensional constant Cd, uniform in the
scale m, contrast Θ, law L, and block vector P.