Coarse-graining support: Support.Deterministic.CoarseCaccioppoli.CrossTerm.Localized

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

Coarse Caccioppoli cross term: localized explicit height

theorem HCPolySupport.coarseCaccioppoli_boundary_noteCrossTermBound_of_localizedExplicitHeightOfScaleChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k : ℝ → ℝ → ℕ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) ⦃ρ₁ ρ₂ : ℝ⦄ : 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → coarseCaccioppoliBoundaryCrossCoeffOfHeight Q a s C uL2Sq (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) ρ₁ ρ₂ ^ 2 ≤ coarseCaccioppoliBoundaryExplicitHeightRecursionRhs Q a s t C uL2Sq * (ρ₂ - ρ₁).rpow (-coarseCaccioppoliBeta s t)

theorem HCPolySupport.coarseCaccioppoli_boundary_noteCrossTermBoundSplit_of_localizedExplicitHeightOfScaleChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) (k : ℝ → ℝ → ℕ) (hCalpha : 0 < Calpha) (hCcross : 0 ≤ Ccross) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) ⦃ρ₁ ρ₂ : ℝ⦄ : 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → coarseCaccioppoliBoundaryCrossCoeffOfHeight Q a s Ccross uL2Sq (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t Calpha k) ρ₁ ρ₂ ^ 2 ≤ coarseCaccioppoliBoundaryExplicitHeightRecursionRhsSplit Q a s t Calpha Ccross uL2Sq * (ρ₂ - ρ₁).rpow (-coarseCaccioppoliBeta s t)