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

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

theorem HCPolySupport.coarseCaccioppoli_boundary_qone_of_preRecurrence {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) {F : ℝ → ℝ} (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hpre : CoarseCaccioppoliBoundaryPreRecurrence Q a s t C uL2Sq F) : F (1 / 3) ≤ coarseCaccioppoliBoundaryBound Q a s t C uL2Sq

Boundary coarse Caccioppoli from the already-absorbed pre-recurrence surface. This is the current next-safe theorem interface before the upstream Besov cutoff/pairing step is formalized.

theorem HCPolySupport.coarseCaccioppoli_boundary_qone_of_explicitHeightPreRecurrence {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) {F : ℝ → ℝ} (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hpre : CoarseCaccioppoliBoundaryExplicitHeightPreRecurrence Q a s t C uL2Sq F) : F (1 / 3) ≤ coarseCaccioppoliBoundaryExplicitHeightBound Q a s t C uL2Sq

Boundary coarse Caccioppoli from the explicit-height pre-recurrence middle layer.

theorem HCPolySupport.coarseCaccioppoli_boundary_qone_of_rawEstimate {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) {F : ℝ → ℝ} {α B : ℝ → ℝ → ℝ} (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hraw : CoarseCaccioppoliBoundaryRawEstimate F α B) (hctrl : CoarseCaccioppoliBoundaryCoefficientControl Q a s t C uL2Sq α B) : F (1 / 3) ≤ coarseCaccioppoliBoundaryBound Q a s t C uL2Sq

Boundary coarse Caccioppoli from the raw local single-cube estimate and the separate coefficient bookkeeping surface.

theorem HCPolySupport.coarseCaccioppoli_boundary_qone_of_noteEstimate {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) {F : ℝ → ℝ} (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hraw : CoarseCaccioppoliBoundaryNoteRawEstimate Q a s t C uL2Sq h F) (hctrl : CoarseCaccioppoliBoundaryNoteCoefficientControl Q a s t C uL2Sq h) : F (1 / 3) ≤ coarseCaccioppoliBoundaryBound Q a s t C uL2Sq

Boundary coarse Caccioppoli from the note-shaped raw estimate and the note-shaped coefficient-control surface.

theorem HCPolySupport.coarseCaccioppoli_boundary_noteCoefficientControl_of_absorptionCondition_of_crossTermBound {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) (habs : CoarseCaccioppoliBoundaryNoteAbsorptionCondition Q a s t C h) (hcross : CoarseCaccioppoliBoundaryNoteCrossTermBound Q a s t C uL2Sq h) : CoarseCaccioppoliBoundaryNoteCoefficientControl Q a s t C uL2Sq h

The split note-specific bookkeeping conditions imply the packaged note-shaped coefficient-control surface.

theorem HCPolySupport.coarseCaccioppoli_boundary_noteCoefficientControl_of_heightChoice_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) (hheight : CoarseCaccioppoliBoundaryHeightChoice Q a s t C h) (hcrossscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 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)) : CoarseCaccioppoliBoundaryNoteCoefficientControl Q a s t C uL2Sq h

The note-facing explicit h choice plus the stronger triadic-scale cross-term estimate recover the packaged boundary coefficient-control surface.

theorem HCPolySupport.coarseCaccioppoli_boundary_qone_of_noteEstimate_of_absorptionCondition_of_crossTermBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) {F : ℝ → ℝ} (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hraw : CoarseCaccioppoliBoundaryNoteRawEstimate Q a s t C uL2Sq h F) (habs : CoarseCaccioppoliBoundaryNoteAbsorptionCondition Q a s t C h) (hcross : CoarseCaccioppoliBoundaryNoteCrossTermBound Q a s t C uL2Sq h) : F (1 / 3) ≤ coarseCaccioppoliBoundaryBound Q a s t C uL2Sq

Boundary coarse Caccioppoli from the note-shaped raw estimate plus the two remaining note-specific bookkeeping obligations.

theorem HCPolySupport.coarseCaccioppoli_boundary_qone_of_noteEstimate_of_absorptionCondition_of_explicitCrossTermBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) {F : ℝ → ℝ} (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hraw : CoarseCaccioppoliBoundaryNoteRawEstimate Q a s t C uL2Sq h F) (habs : CoarseCaccioppoliBoundaryNoteAbsorptionCondition Q a s t C h) (hcross : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → coarseCaccioppoliBoundaryCrossCoeffOfHeight Q a s C uL2Sq h ρ₁ ρ₂ ^ 2 ≤ coarseCaccioppoliBoundaryExplicitHeightRecursionRhs Q a s t C uL2Sq * (ρ₂ - ρ₁).rpow (-coarseCaccioppoliBeta s t)) : F (1 / 3) ≤ coarseCaccioppoliBoundaryExplicitHeightBound Q a s t C uL2Sq

Boundary coarse Caccioppoli with the explicit-height recursion RHS, for any height whose absorption and cross-term square bound have already been proved. This factors out the final radius-iteration step so localized height choices can reuse the same bound.

theorem HCPolySupport.coarseCaccioppoli_boundary_qone_of_noteEstimate_of_heightChoice_of_triadicGapScaleChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) {F : ℝ → ℝ} (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hraw : CoarseCaccioppoliBoundaryNoteRawEstimate Q a s t C uL2Sq h F) (hheight : CoarseCaccioppoliBoundaryHeightChoice Q a s t C h) (hcrossscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 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)) : F (1 / 3) ≤ coarseCaccioppoliBoundaryBound Q a s t C uL2Sq

Boundary coarse Caccioppoli from the note-shaped local estimate, the explicit note-facing h choice, and the remaining stronger triadic-scale cross-term inequality. This is the current closest pre-Besov theorem surface to the note's coefficient-bookkeeping step.

theorem HCPolySupport.coarseCaccioppoli_boundary_qone_of_noteEstimate_of_heightChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k : ℝ → ℝ → ℕ) {F : ℝ → ℝ} (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hraw : CoarseCaccioppoliBoundaryNoteRawEstimate Q a s t C uL2Sq (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k) F) (hcrossscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∃ (j : ℕ), CoarseCaccioppoliTriadicGapScaleChoice j ρ₁ ρ₂ ∧ C * Real.rpow 3 (2 * s * coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k ρ₁ ρ₂) ≤ (C / (s * (1 - s)) * (ThetaRatio Q s t a).rpow (1 / 2)).rpow (coarseCaccioppoliPower s t) * (3 ^ j / 81).rpow (coarseCaccioppoliPower s t)) : F (1 / 3) ≤ coarseCaccioppoliBoundaryBound Q a s t C uL2Sq

Boundary coarse Caccioppoli with the note's actual explicit h = max {k + 4, ceil(...)} height formula, once the caller supplies a triadic scale choice k(ρ₁, ρ₂) and the remaining stronger triadic-scale cross-term estimate.

theorem HCPolySupport.coarseCaccioppoli_boundary_qone_of_noteEstimate_of_explicitHeightOfScaleChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k : ℝ → ℝ → ℕ) {F : ℝ → ℝ} (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hraw : CoarseCaccioppoliBoundaryNoteRawEstimate Q a s t C uL2Sq (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k) F) : F (1 / 3) ≤ coarseCaccioppoliBoundaryExplicitHeightBound Q a s t C uL2Sq

Boundary coarse Caccioppoli in the completed pre-Besov form: once the caller supplies the note-shaped local estimate and the actual explicit height formula h = max {k + 4, ceil(...)}, the remaining coefficient arithmetic is fully internal to this file and no extra cross-scale hypothesis remains.

theorem HCPolySupport.coarseCaccioppoli_boundary_qone_of_noteEstimate_of_localizedExplicitHeightOfScaleChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k : ℝ → ℝ → ℕ) {F : ℝ → ℝ} (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hraw : CoarseCaccioppoliBoundaryNoteRawEstimate Q a s t C uL2Sq (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) F) : F (1 / 3) ≤ coarseCaccioppoliBoundaryExplicitHeightBound Q a s t C uL2Sq

Boundary coarse Caccioppoli with the localized explicit height. This keeps the same final explicit-height bound while adding the scale-localization lower bound h >= 4 / s to the local height.

theorem HCPolySupport.coarseCaccioppoli_boundary_qone_of_heightChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k : ℝ → ℝ → ℕ) {F : ℝ → ℝ} (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hraw : ∀ (n : ℕ), F (coarseCaccioppoliRadiusSequence n) ≤ coarseCaccioppoliBoundaryAlphaOfHeight Q a s t C (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) (coarseCaccioppoliRadiusSequence n) (coarseCaccioppoliRadiusSequence (n + 1)) * F (coarseCaccioppoliRadiusSequence (n + 1)) + coarseCaccioppoliBoundaryCrossCoeffOfHeight Q a s C uL2Sq (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) (coarseCaccioppoliRadiusSequence n) (coarseCaccioppoliRadiusSequence (n + 1)) * √(F (coarseCaccioppoliRadiusSequence (n + 1)))) : F (1 / 3) ≤ coarseCaccioppoliBoundaryExplicitHeightBound Q a s t C uL2Sq

Boundary coarse Caccioppoli from the localized explicit-height note estimate only on the deterministic Chapter-3 radius sequence. This is the concrete iteration surface used when the local cutoff construction is only available for the consecutive pairs (ρ_n, ρ_{n+1}).

theorem HCPolySupport.coarseCaccioppoli_boundary_qone_of_heightChoice_split {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) (k : ℝ → ℝ → ℕ) {F : ℝ → ℝ} (hCalpha : 0 < Calpha) (hCcross : 0 ≤ Ccross) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hraw : ∀ (n : ℕ), F (coarseCaccioppoliRadiusSequence n) ≤ coarseCaccioppoliBoundaryAlphaOfHeight Q a s t Calpha (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t Calpha k) (coarseCaccioppoliRadiusSequence n) (coarseCaccioppoliRadiusSequence (n + 1)) * F (coarseCaccioppoliRadiusSequence (n + 1)) + coarseCaccioppoliBoundaryCrossCoeffOfHeight Q a s Ccross uL2Sq (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t Calpha k) (coarseCaccioppoliRadiusSequence n) (coarseCaccioppoliRadiusSequence (n + 1)) * √(F (coarseCaccioppoliRadiusSequence (n + 1)))) : F (1 / 3) ≤ coarseCaccioppoliBoundaryExplicitHeightBoundSplit Q a s t Calpha Ccross uL2Sq

theorem HCPolySupport.coarseCaccioppoli_boundary_qone_standard_of_noteEstimate {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) (k : ℝ → ℝ → ℕ) {F : ℝ → ℝ} (hCalpha : 0 < Calpha) (hCcross : 0 ≤ Ccross) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hraw : CoarseCaccioppoliBoundaryNoteRawEstimateSplit Q a s t Calpha Ccross uL2Sq (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t Calpha k) F) : F (1 / 3) ≤ coarseCaccioppoliBoundaryExplicitHeightRecursionRhsSplit Q a s t Calpha Ccross uL2Sq * coarseCaccioppoliStandardRadiusIterationConst (coarseCaccioppoliBeta s t)

Boundary coarse Caccioppoli from an all-radii split note-shaped raw estimate, using the standard beta-dependent radius iteration. This is the note-facing iteration endpoint needed to keep the explicit s,t exponents under control.

theorem HCPolySupport.coarseCaccioppoli_boundary_qone_standard_le_noteRhs_of_noteEstimate {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) (k : ℝ → ℝ → ℕ) {F : ℝ → ℝ} (hCalpha : 0 < Calpha) (hCcross : 0 ≤ Ccross) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hTheta : 0 < ThetaRatio Q s t a) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hraw : CoarseCaccioppoliBoundaryNoteRawEstimateSplit Q a s t Calpha Ccross uL2Sq (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t Calpha k) F) : F (1 / 3) ≤ coarseCaccioppoliBoundaryNoteRhs Q a s t (coarseCaccioppoliBoundaryStandardExplicitNoteConstantSplit Q a s t Calpha Ccross) uL2Sq