Coarse-graining support: Support.Deterministic.MultiscaleQuantitiesBasic.Theta #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Boundary-facing theta statements #
theorem
HCPolySupport.thetaRatio_boundary_coefficient_le_of_mem_descendantsAtScale
{d : ℕ}
{Q R : TriadicCube d}
{k : ℤ}
(a : CoeffField d)
(s t : ℝ)
(hs : 0 ≤ s)
(ht : 0 ≤ t)
(hR : R ∈ descendantsAtScale Q k)
(hBsum :
Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hSigmaSum :
Summable fun (n : ℕ) =>
geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
theorem
HCPolySupport.weighted_descendant_product_sq_le_thetaRatio
{d : ℕ}
{Q R : TriadicCube d}
{k : ℤ}
(a : CoeffField d)
(s t : ℝ)
(hs : 0 ≤ s)
(ht : 0 ≤ t)
(hR : R ∈ descendantsAtScale Q k)
(hBsum :
Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hSigmaSum :
Summable fun (n : ℕ) =>
geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
(geometricWeight s 1 (Q.scale - k).toNat * (coarseBBlockNorm R a).rpow (1 / 2) * (geometricWeight t 1 (Q.scale - k).toNat * (coarseSigmaStarInvBlockNorm R a).rpow (1 / 2))) ^ 2 ≤ ThetaRatio Q s t a