Coarse-graining support: Support.Deterministic.CoarseCaccioppoli.CrossTerm.Scalar #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Coarse Caccioppoli cross term: scalar bounds #
theorem
HCPolySupport.coarseCaccioppoliBoundaryCrossCoeffOfHeight_sq
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(s C uL2Sq : ℝ)
(h : ℝ → ℝ → ℝ)
{ρ₁ ρ₂ : ℝ}
(hs : 0 ≤ s)
(hu : 0 ≤ uL2Sq)
:
coarseCaccioppoliBoundaryCrossCoeffOfHeight Q a s C uL2Sq h ρ₁ ρ₂ ^ 2 = C * coarseCaccioppoliGapInv ρ₁ ρ₂ ^ 2 * LambdaSq Q s (MultiscaleExponent.finite 1) a * uL2Sq * (C * Real.rpow 3 (2 * s * h ρ₁ ρ₂))
theorem
HCPolySupport.coarseCaccioppoli_boundary_explicitHeight_leftBranch_scalar
{ρ₁ ρ₂ s C : ℝ}
{k : ℕ}
(hC : 0 ≤ C)
(hs : 0 < s)
(hs1 : s < 1)
(hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂)
(hlt : ρ₁ < ρ₂)
:
theorem
HCPolySupport.coarseCaccioppoli_boundary_explicitHeight_rightBranch_scalar
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
{ρ₁ ρ₂ s t C : ℝ}
{k : ℕ}
(hC : 0 ≤ C)
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂)
(hlt : ρ₁ < ρ₂)
(hbranch :
↑k + 4 < ↑⌈Real.log (coarseCaccioppoliBoundaryHeightLogArg Q a s t C k) / (coarseCaccioppoliSigma s t * Real.log 3)⌉₊)
:
C * Real.rpow 3
(2 * s * ↑⌈Real.log (coarseCaccioppoliBoundaryHeightLogArg Q a s t C k) / (coarseCaccioppoliSigma s t * Real.log 3)⌉₊) ≤ 9 * Real.rpow 4 (coarseCaccioppoliPower s t) * Real.rpow 81 (coarseCaccioppoliPower s t) * C * (C / (s * (1 - s)) * (ThetaRatio Q s t a).rpow (1 / 2)).rpow (coarseCaccioppoliPower s t) * (coarseCaccioppoliGapInv ρ₁ ρ₂).rpow (coarseCaccioppoliPower s t)
theorem
HCPolySupport.coarseCaccioppoli_boundary_explicitHeight_rightBranch_scalar_with_front
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
{ρ₁ ρ₂ s t Calpha Ccross : ℝ}
{k : ℕ}
(hCalpha : 0 < Calpha)
(hCcross : 0 ≤ Ccross)
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂)
(hlt : ρ₁ < ρ₂)
(hbranch :
↑k + 4 < ↑⌈Real.log (coarseCaccioppoliBoundaryHeightLogArg Q a s t Calpha k) / (coarseCaccioppoliSigma s t * Real.log 3)⌉₊)
:
Ccross * Real.rpow 3
(2 * s * ↑⌈Real.log (coarseCaccioppoliBoundaryHeightLogArg Q a s t Calpha k) / (coarseCaccioppoliSigma s t * Real.log 3)⌉₊) ≤ 9 * Real.rpow 4 (coarseCaccioppoliPower s t) * Real.rpow 81 (coarseCaccioppoliPower s t) * Ccross * (Calpha / (s * (1 - s)) * (ThetaRatio Q s t a).rpow (1 / 2)).rpow (coarseCaccioppoliPower s t) * (coarseCaccioppoliGapInv ρ₁ ρ₂).rpow (coarseCaccioppoliPower s t)
theorem
HCPolySupport.coarseCaccioppoli_boundary_noteCrossTermBound_of_triadicGapScaleChoice
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
(h : ℝ → ℝ → ℝ)
(hC : 0 ≤ C)
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hu : 0 ≤ uL2Sq)
(hscale :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
∃ (k : ℕ),
CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂ ∧ C * Real.rpow 3 (2 * s * h ρ₁ ρ₂) ≤ (C / (s * (1 - s)) * (ThetaRatio Q s t a).rpow (1 / 2)).rpow (coarseCaccioppoliPower s t) * (3 ^ k / 81).rpow (coarseCaccioppoliPower s t))
:
CoarseCaccioppoliBoundaryNoteCrossTermBound Q a s t C uL2Sq h
A stronger triadic-scale cross-term estimate, stated using the note's
auxiliary scale k, implies the actual cross-term square bound appearing in
the boundary coefficient bookkeeping.