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

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

Coarse Caccioppoli cross term: explicit height

theorem HCPolySupport.coarseCaccioppoli_interior_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)) : CoarseCaccioppoliInteriorNoteCrossTermBound Q a s t C uL2Sq h

The interior note-specific cross-term bound currently follows from the same stronger triadic-scale estimate as the boundary version.

theorem HCPolySupport.coarseCaccioppoli_boundary_noteCrossTermBound_of_explicitHeightOfScaleChoice {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 (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k) ρ₁ ρ₂ ^ 2 ≤ coarseCaccioppoliBoundaryExplicitHeightRecursionRhs Q a s t C uL2Sq * (ρ₂ - ρ₁).rpow (-coarseCaccioppoliBeta s t)

The note's actual explicit height choice h = max {k + 4, ceil(...)} gives an honest pre-Besov cross-term square bound with a split recursive prefactor: one branch comes from k + 4, the other from the logarithmic ceiling.

theorem HCPolySupport.coarseCaccioppoli_boundary_noteCrossTermBoundSplit_of_explicitHeightOfScaleChoice {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 (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t Calpha k) ρ₁ ρ₂ ^ 2 ≤ coarseCaccioppoliBoundaryExplicitHeightRecursionRhsSplit Q a s t Calpha Ccross uL2Sq * (ρ₂ - ρ₁).rpow (-coarseCaccioppoliBeta s t)