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

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

theorem HCPolySupport.coarseCaccioppoliInteriorNoteRhs_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) : 0 ≤ coarseCaccioppoliInteriorNoteRhs Q a s t C uL2Sq

theorem HCPolySupport.coarseCaccioppoliInteriorNoteRhs_mono_C {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C₁ C₂ uL2Sq : ℝ) (hC₁ : 0 ≤ C₁) (hC₁C₂ : C₁ ≤ C₂) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) : coarseCaccioppoliInteriorNoteRhs Q a s t C₁ uL2Sq ≤ coarseCaccioppoliInteriorNoteRhs Q a s t C₂ uL2Sq

theorem HCPolySupport.coarseCaccioppoliInteriorNoteRhs_mul_const_le_of_mul_constant_le {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t M C₁ C₂ uL2Sq : ℝ) (hM : 1 ≤ M) (hC₁ : 0 ≤ C₁) (hMC₁C₂ : M * C₁ ≤ C₂) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) : M * coarseCaccioppoliInteriorNoteRhs Q a s t C₁ uL2Sq ≤ coarseCaccioppoliInteriorNoteRhs Q a s t C₂ uL2Sq

theorem HCPolySupport.coarseCaccioppoliBoundaryRecursionRhs_eq_zero_of_uL2Sq_eq_zero {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (hu : uL2Sq = 0) : coarseCaccioppoliBoundaryRecursionRhs Q a s t C uL2Sq = 0

theorem HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightRecursionRhs_eq_zero_of_uL2Sq_eq_zero {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (hu : uL2Sq = 0) : coarseCaccioppoliBoundaryExplicitHeightRecursionRhs Q a s t C uL2Sq = 0

theorem HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightBound_eq_zero_of_uL2Sq_eq_zero {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (hu : uL2Sq = 0) : coarseCaccioppoliBoundaryExplicitHeightBound Q a s t C uL2Sq = 0

theorem HCPolySupport.coarseCaccioppoliBoundaryNoteRhs_eq_zero_of_uL2Sq_eq_zero {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (hu : uL2Sq = 0) : coarseCaccioppoliBoundaryNoteRhs Q a s t C uL2Sq = 0

theorem HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightBound_le_noteRhs_of_uL2Sq_eq_zero {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Cinternal Cnote uL2Sq : ℝ) (hu : uL2Sq = 0) : coarseCaccioppoliBoundaryExplicitHeightBound Q a s t Cinternal uL2Sq ≤ coarseCaccioppoliBoundaryNoteRhs Q a s t Cnote uL2Sq

theorem HCPolySupport.coarseCaccioppoliInteriorExplicitHeightBound_le_noteRhs_of_uL2Sq_eq_zero {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Cinternal Cnote uL2Sq : ℝ) (hu : uL2Sq = 0) : coarseCaccioppoliInteriorExplicitHeightBound Q a s t Cinternal uL2Sq ≤ coarseCaccioppoliInteriorNoteRhs Q a s t Cnote uL2Sq

theorem HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightBound_le_noteRhs_of_coeff_le {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Cinternal Cnote uL2Sq : ℝ) (hcoeff : coarseCaccioppoliBoundaryExplicitHeightCoeff Q a s t Cinternal ≤ coarseCaccioppoliBoundaryNoteCoeff Q a s t Cnote) (hu : 0 ≤ uL2Sq) : coarseCaccioppoliBoundaryExplicitHeightBound Q a s t Cinternal uL2Sq ≤ coarseCaccioppoliBoundaryNoteRhs Q a s t Cnote uL2Sq

theorem HCPolySupport.coarseCaccioppoliInteriorExplicitHeightBound_le_noteRhs_of_coeff_le {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Cinternal Cnote uL2Sq : ℝ) (hcoeff : coarseCaccioppoliBoundaryExplicitHeightCoeff Q a s t Cinternal ≤ coarseCaccioppoliBoundaryNoteCoeff Q a s t Cnote) (hu : 0 ≤ uL2Sq) : coarseCaccioppoliInteriorExplicitHeightBound Q a s t Cinternal uL2Sq ≤ coarseCaccioppoliInteriorNoteRhs Q a s t Cnote uL2Sq

theorem HCPolySupport.coarseCaccioppoliBoundaryHeightBound_le_noteRhs {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Cinternal Cadequate Cnote uL2Sq : ℝ) (hcoeff : coarseCaccioppoliBoundaryExplicitHeightCoeff Q a s t Cinternal ≤ coarseCaccioppoliBoundaryNoteCoeff Q a s t Cadequate) (hCadequate : 0 ≤ Cadequate) (hCadequateCnote : Cadequate ≤ Cnote) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) : coarseCaccioppoliBoundaryExplicitHeightBound Q a s t Cinternal uL2Sq ≤ coarseCaccioppoliBoundaryNoteRhs Q a s t Cnote uL2Sq

theorem HCPolySupport.coarseCaccioppoliInteriorExplicitHeightBound_le_noteRhs_of_coeff_le_noteCoeff_of_noteConstant_le {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Cinternal Cadequate Cnote uL2Sq : ℝ) (hcoeff : coarseCaccioppoliBoundaryExplicitHeightCoeff Q a s t Cinternal ≤ coarseCaccioppoliBoundaryNoteCoeff Q a s t Cadequate) (hCadequate : 0 ≤ Cadequate) (hCadequateCnote : Cadequate ≤ Cnote) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) : coarseCaccioppoliInteriorExplicitHeightBound Q a s t Cinternal uL2Sq ≤ coarseCaccioppoliInteriorNoteRhs Q a s t Cnote uL2Sq

theorem HCPolySupport.coarseCaccioppoliBoundaryCoeff_le_of_explicitHeightBound_le_noteRhs {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Cinternal Cnote uL2Sq : ℝ) (hu : 0 < uL2Sq) (h : coarseCaccioppoliBoundaryExplicitHeightBound Q a s t Cinternal uL2Sq ≤ coarseCaccioppoliBoundaryNoteRhs Q a s t Cnote uL2Sq) : coarseCaccioppoliBoundaryExplicitHeightCoeff Q a s t Cinternal ≤ coarseCaccioppoliBoundaryNoteCoeff Q a s t Cnote

theorem HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightBound_le_noteRhs_iff_coeff_le {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Cinternal Cnote uL2Sq : ℝ) (hu : 0 < uL2Sq) : coarseCaccioppoliBoundaryExplicitHeightBound Q a s t Cinternal uL2Sq ≤ coarseCaccioppoliBoundaryNoteRhs Q a s t Cnote uL2Sq ↔ coarseCaccioppoliBoundaryExplicitHeightCoeff Q a s t Cinternal ≤ coarseCaccioppoliBoundaryNoteCoeff Q a s t Cnote

theorem HCPolySupport.coarseCaccioppoli_boundary_qone_of_radius_recurrence {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) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hrec : CoarseCaccioppoliRadiusRecurrence F (coarseCaccioppoliBoundaryRecursionRhs Q a s t C uL2Sq) (coarseCaccioppoliBeta s t)) : F (1 / 3) ≤ coarseCaccioppoliBoundaryBound Q a s t C uL2Sq

Boundary coarse Caccioppoli in the current honest Chapter-3 form: once the local cutoff/Besov step has produced the radius-recursion with the note-facing multiscale prefactor, the deterministic radius iteration yields the final boundary bound.

theorem HCPolySupport.coarseCaccioppoli_boundary_preRecurrence_of_rawEstimate {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) {F : ℝ → ℝ} {α B : ℝ → ℝ → ℝ} (hraw : CoarseCaccioppoliBoundaryRawEstimate F α B) (hctrl : CoarseCaccioppoliBoundaryCoefficientControl Q a s t C uL2Sq α B) : CoarseCaccioppoliBoundaryPreRecurrence Q a s t C uL2Sq F

The local single-cube estimate plus coefficient bookkeeping imply the already-absorbed pre-recurrence surface. This is the current pre-Besov bridge between the note's local estimate and the iteration backbone.

theorem HCPolySupport.coarseCaccioppoli_boundary_preRecurrence_of_noteEstimate {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) {F : ℝ → ℝ} (hraw : CoarseCaccioppoliBoundaryNoteRawEstimate Q a s t C uL2Sq h F) (hctrl : CoarseCaccioppoliBoundaryNoteCoefficientControl Q a s t C uL2Sq h) : CoarseCaccioppoliBoundaryPreRecurrence Q a s t C uL2Sq F

Boundary pre-recurrence from the note-shaped raw estimate and note-shaped coefficient-control surface.

theorem HCPolySupport.coarseCaccioppoli_boundary_preRecurrence_of_absorbedCrossTerm {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) (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) : CoarseCaccioppoliBoundaryPreRecurrence Q a s t C uL2Sq F

Boundary pre-recurrence from the note-shaped raw estimate plus the two remaining note-specific bookkeeping obligations.

theorem HCPolySupport.coarseCaccioppoli_boundary_explicitHeightPreRecurrence_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) (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)) : CoarseCaccioppoliBoundaryExplicitHeightPreRecurrence Q a s t C uL2Sq F

Explicit-height pre-recurrence from a note-shaped raw estimate, absorption, and the enlarged explicit-height cross-term square bound.

theorem HCPolySupport.coarseCaccioppoli_boundary_radius_recurrence_of_preRecurrence {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) {F : ℝ → ℝ} (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hpre : CoarseCaccioppoliBoundaryPreRecurrence Q a s t C uL2Sq F) : CoarseCaccioppoliRadiusRecurrence F (coarseCaccioppoliBoundaryRecursionRhs Q a s t C uL2Sq) (coarseCaccioppoliBeta s t)

The pre-recurrence middle layer of the boundary proof implies the abstract radius-recursion used by the deterministic iteration backbone.

theorem HCPolySupport.coarseCaccioppoli_boundary_radius_recurrence_of_explicitHeightPreRecurrence {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) {F : ℝ → ℝ} (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hpre : CoarseCaccioppoliBoundaryExplicitHeightPreRecurrence Q a s t C uL2Sq F) : CoarseCaccioppoliRadiusRecurrence F (coarseCaccioppoliBoundaryExplicitHeightRecursionRhs Q a s t C uL2Sq) (coarseCaccioppoliBeta s t)

Explicit-height pre-recurrence implies the radius recurrence with the enlarged explicit-height prefactor.