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

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

theorem HCPolySupport.coarseCaccioppoli_boundary_noteRawEstimate_of_radiusEnergyBridgeInputs {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) {F : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B : ℝ → ℝ → ℝ) (hs0 : 0 < s) (hs1 : s < 1) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq k h F flux u g ξ energy Acirc1 AcircS B) (hctrl : CoarseCaccioppoliBoundarySingleCubeToRawCoefficientControl Q a s t C uL2Sq k h F) : CoarseCaccioppoliBoundaryNoteRawEstimate Q a s t C uL2Sq h F

Radius-indexed energy bridge inputs plus the single-cube-to-raw coefficient-localization controls produce the note-shaped raw radius estimate.

theorem HCPolySupport.coarseCaccioppoli_boundary_rawEstimate_of_radiusBridge_localized {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) {F : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B : ℝ → ℝ → ℝ) (hs0 : 0 < s) (hs1 : s < 1) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq k h F flux u g ξ energy Acirc1 AcircS B) (hloc : CoarseCaccioppoliBoundarySingleCubeCoefficientLocalization Q a s t C uL2Sq k h) : CoarseCaccioppoliBoundaryNoteRawEstimate Q a s t C uL2Sq h F

Radius-indexed energy bridge inputs produce the note-shaped raw estimate from pure coefficient-localization data plus nonnegativity of the radius energy.

theorem HCPolySupport.coarseCaccioppoli_boundary_noteRawEstimate_of_radiusEnergyBridgeInputs_of_scale_of_ellipticity {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) {F : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs0 : 0 < s) (hs1 : s < 1) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq k h F flux u g ξ energy Acirc1 AcircS B) (hscaleLoc : CoarseCaccioppoliBoundarySingleCubeScaleLocalization s t k h) (helliptic : CoarseCaccioppoliBoundarySingleCubeEllipticityLocalization Q a s t) : CoarseCaccioppoliBoundaryNoteRawEstimate Q a s t C uL2Sq h F

Raw boundary note estimate from the primitive scale and ellipticity localization inputs.

theorem HCPolySupport.coarseCaccioppoli_boundary_noteEstimate_of_radiusEnergyInputs {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) {lam Lam : ℝ} (k : ℝ → ℝ → ℕ) {F : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) F flux u g ξ energy Acirc1 AcircS B) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ R ∈ descendantsAtScale Q j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (hBsum_s : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hSigmaSum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : CoarseCaccioppoliBoundaryNoteRawEstimate Q a s t C uL2Sq (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) F

Raw boundary note estimate from radius-indexed energy bridge inputs using the localized explicit height and the standard multiscale ellipticity data.

theorem HCPolySupport.coarseCaccioppoli_boundary_explicitHeightPreRecurrence_of_radiusEnergyInputs {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) {lam Lam : ℝ} (k : ℝ → ℝ → ℕ) {F : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) F flux u g ξ energy Acirc1 AcircS B) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ R ∈ descendantsAtScale Q j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (hBsum_s : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hSigmaSum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : CoarseCaccioppoliBoundaryExplicitHeightPreRecurrence Q a s t C uL2Sq F

Explicit-height boundary pre-recurrence from radius-indexed energy bridge inputs using the localized explicit height and standard multiscale ellipticity data.

theorem HCPolySupport.coarseCaccioppoli_boundary_noteEstimate_of_multiscaleEllipticity {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) {lam Lam : ℝ} (k : ℝ → ℝ → ℕ) {F : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B U Xi D A1 AS : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalFactorInputs Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) F flux u g ξ energy Acirc1 AcircS B U Xi D A1 AS) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ R ∈ descendantsAtScale Q j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (hBsum_s : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hSigmaSum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : CoarseCaccioppoliBoundaryNoteRawEstimate Q a s t C uL2Sq (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) F

Raw boundary note estimate from canonical LambdaSq factor inputs using the localized explicit height and standard multiscale ellipticity data.

theorem HCPolySupport.coarseCaccioppoli_boundary_explicitHeightPreRecurrence_of_heightChoice {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) {lam Lam : ℝ} (k : ℝ → ℝ → ℕ) {F : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B U Xi D A1 AS : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalFactorInputs Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) F flux u g ξ energy Acirc1 AcircS B U Xi D A1 AS) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ R ∈ descendantsAtScale Q j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (hBsum_s : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hSigmaSum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : CoarseCaccioppoliBoundaryExplicitHeightPreRecurrence Q a s t C uL2Sq F

Boundary explicit-height pre-recurrence from canonical LambdaSq factor inputs using localized explicit height and standard multiscale ellipticity data.

theorem HCPolySupport.coarseCaccioppoli_boundary_preRecurrence_of_radiusEnergyBridgeInputs {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) {F : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq k h F flux u g ξ energy Acirc1 AcircS B) (hctrl : CoarseCaccioppoliBoundarySingleCubeToRawCoefficientControl Q a s t C uL2Sq k 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

The same radius-indexed energy bridge inputs also feed the absorbed pre-recurrence layer, once the note-specific absorption and cross-term bookkeeping are available.

theorem HCPolySupport.coarseCaccioppoli_boundary_preRecurrence_of_radiusEnergyBridgeInputs_of_coefficientLocalization {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) {F : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq k h F flux u g ξ energy Acirc1 AcircS B) (hloc : CoarseCaccioppoliBoundarySingleCubeCoefficientLocalization Q a s t C uL2Sq k h) (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 radius-indexed energy bridge inputs and pure coefficient localization.

theorem HCPolySupport.coarseCaccioppoli_boundary_preRecurrence_of_radiusEnergyBridgeInputs_of_scale_of_ellipticity {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) {F : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq k h F flux u g ξ energy Acirc1 AcircS B) (hscaleLoc : CoarseCaccioppoliBoundarySingleCubeScaleLocalization s t k h) (helliptic : CoarseCaccioppoliBoundarySingleCubeEllipticityLocalization Q a s t) (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 primitive scale and ellipticity localization inputs.

theorem HCPolySupport.coarseCaccioppoli_boundary_qone_of_singleCubeRawEstimate_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 ρ₁ ρ₂) ρ₁ ρ₂) (hsingle : CoarseCaccioppoliBoundarySingleCubeRawEstimate Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k) F) (hctrl : CoarseCaccioppoliBoundarySingleCubeToRawCoefficientControl Q a s t C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k) F) : F (1 / 3) ≤ coarseCaccioppoliBoundaryExplicitHeightBound Q a s t C uL2Sq

Boundary coarse Caccioppoli from radius-indexed single-cube estimates, explicit-height choice, and the single-cube-to-raw coefficient-localization controls.

theorem HCPolySupport.coarseCaccioppoli_boundary_qone_of_radiusEnergyBridgeInputs_of_explicitHeightOfScaleChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k : ℝ → ℝ → ℕ) {F : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS 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) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k) F flux u g ξ energy Acirc1 AcircS B) (hctrl : CoarseCaccioppoliBoundarySingleCubeToRawCoefficientControl Q a s t C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k) F) : F (1 / 3) ≤ coarseCaccioppoliBoundaryExplicitHeightBound Q a s t C uL2Sq

Boundary coarse Caccioppoli directly from the radius-indexed energy bridge inputs, explicit-height choice, and the single-cube-to-raw coefficient-localization controls.

theorem HCPolySupport.coarseCaccioppoli_boundary_qone_of_radiusEnergyInputs_of_heightChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k : ℝ → ℝ → ℕ) {F : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS 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) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k) F flux u g ξ energy Acirc1 AcircS B) (hloc : CoarseCaccioppoliBoundarySingleCubeCoefficientLocalization Q a s t C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k)) : F (1 / 3) ≤ coarseCaccioppoliBoundaryExplicitHeightBound Q a s t C uL2Sq

Boundary coarse Caccioppoli from radius-indexed energy bridge inputs and pure coefficient-localization data. This is the same as coarseCaccioppoli_boundary_qone_of_radiusEnergyBridgeInputs_of_explicitHeightOfScaleChoice, but it assembles the mixed single-cube-to-raw coefficient-control bundle from the already-available nonnegativity hypothesis.

theorem HCPolySupport.coarseCaccioppoli_boundary_qone_of_radiusEnergyInputs_of_scale {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k : ℝ → ℝ → ℕ) {F : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS 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) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k) F flux u g ξ energy Acirc1 AcircS B) (hscaleLoc : CoarseCaccioppoliBoundarySingleCubeScaleLocalization s t (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k)) (helliptic : CoarseCaccioppoliBoundarySingleCubeEllipticityLocalization Q a s t) : F (1 / 3) ≤ coarseCaccioppoliBoundaryExplicitHeightBound Q a s t C uL2Sq

Boundary coarse Caccioppoli from the two primitive localization inputs: the scale-only radius inequality and the ellipticity-only comparison.

theorem HCPolySupport.coarseCaccioppoli_boundary_qone_of_radiusEnergyInputs_of_heightChoice_of_lower {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) {lam Lam : ℝ} (k : ℝ → ℝ → ℕ) {F : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS 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) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hheight_const : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → 4 / s ≤ coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k ρ₁ ρ₂) (hheight_cent : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → 4 / (s + t) ≤ coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k ρ₁ ρ₂) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k) F flux u g ξ energy Acirc1 AcircS B) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ R ∈ descendantsAtScale Q j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (hBsum_s : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hSigmaSum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : F (1 / 3) ≤ coarseCaccioppoliBoundaryExplicitHeightBound Q a s t C uL2Sq

Boundary coarse Caccioppoli from radius-indexed energy bridge inputs and fully composed localization data: triadic gap scale choice, concrete lower bounds on the explicit height, and the standard multiscale ellipticity data.

theorem HCPolySupport.coarseCaccioppoli_boundary_qone_of_radiusEnergyInputs_of_of_radiusEnergyInputs {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) {lam Lam : ℝ} (k : ℝ → ℝ → ℕ) {F : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS 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) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) F flux u g ξ energy Acirc1 AcircS B) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ R ∈ descendantsAtScale Q j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (hBsum_s : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hSigmaSum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : F (1 / 3) ≤ coarseCaccioppoliBoundaryExplicitHeightBound Q a s t C uL2Sq

Boundary coarse Caccioppoli from radius-indexed energy bridge inputs using the localized explicit height. The localized height supplies the scale-side lower bounds internally, so callers only provide the triadic gap choice and the standard multiscale ellipticity data.