Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicFinal.Endpoints

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

Theorem-facing Caccioppoli endpoint aliases

This file keeps the theorem-facing endpoint aliases separate from the internal InputSpecializations bridge machinery. It retains only the standard beta-dependent split endpoint route and the scalar budgets needed to construct that route internally.

noncomputable def HCPolySupport.coarseCaccioppoliLocalPatchBufferedCutoffBudget {d : ℕ} (Q : TriadicCube d) : ℝ

Explicit local-patch cutoff budget for the buffered boundary route.

This is the cutoff-size term formerly hidden inside an existential choice of Clocal. Keeping it as a definition lets later public theorems bound the resulting note constant without losing track of which max construction was used.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.coarseCaccioppoliLocalPatchBufferedCutoffBudgetUnit (d : ℕ) : ℝ

The local-patch cutoff budget on a scale-zero cube, written without cube geometry parameters.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.coarseCaccioppoliLocalPatchBufferedCutoffBudget_eq_unit_of_scale_eq_zero {d : ℕ} {Q : TriadicCube d} (hQ : Q.scale = 0) : coarseCaccioppoliLocalPatchBufferedCutoffBudget Q = coarseCaccioppoliLocalPatchBufferedCutoffBudgetUnit d

noncomputable def HCPolySupport.coarseCaccioppoliLocalPatchBufferedLocalBudget {d : ℕ} (Q : TriadicCube d) (Csol : ℝ) : ℝ

Explicit Clocal used by the local-patch buffered boundary endpoint.

Equations

• HCPolySupport.coarseCaccioppoliLocalPatchBufferedLocalBudget Q Csol = max 1 (max Csol (HCPolySupport.coarseCaccioppoliLocalPatchBufferedCutoffBudget Q))

noncomputable def HCPolySupport.coarseCaccioppoliLocalPatchBufferedCeffLocalBudget {d : ℕ} (Q : TriadicCube d) (Csol : ℝ) : ℝ

Effective local budget after summing over coordinate directions.

Equations

• HCPolySupport.coarseCaccioppoliLocalPatchBufferedCeffLocalBudget Q Csol = ↑(Fintype.card (Fin d)) * HCPolySupport.coarseCaccioppoliLocalPatchBufferedLocalBudget Q Csol

noncomputable def HCPolySupport.coarseCaccioppoliLocalPatchBufferedCenteredFrontBudget {d : ℕ} (Q : TriadicCube d) (s Csol : ℝ) : ℝ

Centered-front budget used by the arbitrary-center local-patch route.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.coarseCaccioppoliLocalPatchBufferedAlphaBudget {d : ℕ} (Q : TriadicCube d) (s Csol : ℝ) : ℝ

Split alpha/front budget used by the local-patch buffered boundary endpoint.

Equations

• HCPolySupport.coarseCaccioppoliLocalPatchBufferedAlphaBudget Q s Csol = max 1 (81 * HCPolySupport.coarseCaccioppoliLocalPatchBufferedCenteredFrontBudget Q s Csol * (s * (1 - s)))

noncomputable def HCPolySupport.coarseCaccioppoliLocalPatchBufferedCrossBudget {d : ℕ} (Q : TriadicCube d) (s Csol : ℝ) : ℝ

Split constant/cross budget used by the local-patch buffered boundary endpoint.

Equations

• HCPolySupport.coarseCaccioppoliLocalPatchBufferedCrossBudget Q s Csol = max 1 (81 * Real.rpow 3 (2 * s) * HCPolySupport.coarseCaccioppoliLocalPatchBufferedLocalBudget Q Csol)

noncomputable def HCPolySupport.coarseCaccioppoliLocalPatchBufferedAlphaBudgetUnit (d : ℕ) (s : ℝ) : ℝ

Unit-cube split alpha/front budget for the local-patch boundary route.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.coarseCaccioppoliLocalPatchBufferedCrossBudgetUnit (d : ℕ) (s : ℝ) : ℝ

Unit-cube split constant/cross budget for the local-patch boundary route.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.coarseCaccioppoliLocalPatchBufferedAlphaBudget_eq_unit_of_scale_eq_zero {d : ℕ} {Q : TriadicCube d} (s : ℝ) (hQ : Q.scale = 0) : coarseCaccioppoliLocalPatchBufferedAlphaBudget Q s (fullVectorPoincareCubeConstant Q) = coarseCaccioppoliLocalPatchBufferedAlphaBudgetUnit d s

theorem HCPolySupport.coarseCaccioppoliLocalPatchBufferedCrossBudget_eq_unit_of_scale_eq_zero {d : ℕ} {Q : TriadicCube d} (s : ℝ) (hQ : Q.scale = 0) : coarseCaccioppoliLocalPatchBufferedCrossBudget Q s (fullVectorPoincareCubeConstant Q) = coarseCaccioppoliLocalPatchBufferedCrossBudgetUnit d s

theorem HCPolySupport.coarseCaccioppoliLocalPatchBufferedBudgetSplit_spec {d : ℕ} [NeZero d] (Q : TriadicCube d) (s t Csol : ℝ) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) : Csol ≤ coarseCaccioppoliLocalPatchBufferedLocalBudget Q Csol ∧ 0 ≤ coarseCaccioppoliLocalPatchBufferedLocalBudget Q Csol ∧ 0 < coarseCaccioppoliLocalPatchBufferedAlphaBudget Q s Csol ∧ 0 ≤ coarseCaccioppoliLocalPatchBufferedCrossBudget Q s Csol ∧ 81 * Real.rpow 3 (2 * s) * (↑(Fintype.card (Fin d)) * coarseCaccioppoliLocalPatchBufferedLocalBudget Q Csol) ≤ ↑(Fintype.card (Fin d)) * coarseCaccioppoliLocalPatchBufferedCrossBudget Q s Csol ∧ 81 * (6 * coarseCaccioppoliCenteredAverageFront d s (↑(Fintype.card (Fin d)) * coarseCaccioppoliLocalPatchBufferedLocalBudget Q Csol) + 12 * coarseCaccioppoliCenteredBesovHessianFront d s (↑(Fintype.card (Fin d)) * coarseCaccioppoliLocalPatchBufferedLocalBudget Q Csol) + 6 * coarseCaccioppoliCenteredBesovGradientFront d s (↑(Fintype.card (Fin d)) * coarseCaccioppoliLocalPatchBufferedLocalBudget Q Csol)) ≤ ↑(Fintype.card (Fin d)) * coarseCaccioppoliLocalPatchBufferedAlphaBudget Q s Csol / (s * (1 - s)) ∧ coarseCaccioppoliLocalPatchBufferedCutoffBudget Q ≤ ↑(Fintype.card (Fin d)) * coarseCaccioppoliLocalPatchBufferedLocalBudget Q Csol

The explicit split local-patch buffered budgets satisfy the scalar side conditions needed by the split exact raw-coefficient package.

noncomputable def HCPolySupport.coarseCaccioppoliBufferedCutoffBudget {d : ℕ} (Q : TriadicCube d) : ℝ

Explicit cutoff budget for the centered buffered route.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.coarseCaccioppoliBufferedCutoffBudgetUnit (d : ℕ) : ℝ

The centered buffered cutoff budget on a scale-zero cube, written without cube geometry parameters.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.coarseCaccioppoliBufferedCutoffBudget_eq_unit_of_scale_eq_zero {d : ℕ} {Q : TriadicCube d} (hQ : Q.scale = 0) : coarseCaccioppoliBufferedCutoffBudget Q = coarseCaccioppoliBufferedCutoffBudgetUnit d

noncomputable def HCPolySupport.coarseCaccioppoliBufferedLocalBudget {d : ℕ} (Q : TriadicCube d) (Csol : ℝ) : ℝ

Explicit Clocal used by the centered buffered endpoint.

Equations

• HCPolySupport.coarseCaccioppoliBufferedLocalBudget Q Csol = max 1 (max Csol (HCPolySupport.coarseCaccioppoliBufferedCutoffBudget Q))

noncomputable def HCPolySupport.coarseCaccioppoliBufferedCeffLocalBudget {d : ℕ} (Q : TriadicCube d) (Csol : ℝ) : ℝ

Effective centered buffered local budget after summing directions.

Equations

• HCPolySupport.coarseCaccioppoliBufferedCeffLocalBudget Q Csol = ↑(Fintype.card (Fin d)) * HCPolySupport.coarseCaccioppoliBufferedLocalBudget Q Csol

noncomputable def HCPolySupport.coarseCaccioppoliBufferedCenteredFrontBudget {d : ℕ} (Q : TriadicCube d) (s Csol : ℝ) : ℝ

Centered-front budget used by the centered buffered route.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.coarseCaccioppoliBufferedAlphaBudget {d : ℕ} (Q : TriadicCube d) (s Csol : ℝ) : ℝ

Split alpha/front budget used by the centered buffered endpoint.

Equations

• HCPolySupport.coarseCaccioppoliBufferedAlphaBudget Q s Csol = max 1 (81 * HCPolySupport.coarseCaccioppoliBufferedCenteredFrontBudget Q s Csol * (s * (1 - s)))

noncomputable def HCPolySupport.coarseCaccioppoliBufferedCrossBudget {d : ℕ} (Q : TriadicCube d) (s Csol : ℝ) : ℝ

Split constant/cross budget used by the centered buffered endpoint.

Equations

• HCPolySupport.coarseCaccioppoliBufferedCrossBudget Q s Csol = max 1 (81 * Real.rpow 3 s * HCPolySupport.coarseCaccioppoliBufferedLocalBudget Q Csol)

noncomputable def HCPolySupport.coarseCaccioppoliBufferedAlphaBudgetUnit (d : ℕ) (s : ℝ) : ℝ

Unit-cube centered buffered alpha/front budget, depending only on d and s.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.coarseCaccioppoliBufferedCrossBudgetUnit (d : ℕ) (s : ℝ) : ℝ

Unit-cube centered buffered constant/cross budget, depending only on d and s.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.coarseCaccioppoliBufferedAlphaBudget_eq_unit_of_scale_eq_zero {d : ℕ} {Q : TriadicCube d} (s : ℝ) (hQ : Q.scale = 0) : coarseCaccioppoliBufferedAlphaBudget Q s (fullVectorPoincareCubeConstant Q) = coarseCaccioppoliBufferedAlphaBudgetUnit d s

theorem HCPolySupport.coarseCaccioppoliBufferedCrossBudget_eq_unit_of_scale_eq_zero {d : ℕ} {Q : TriadicCube d} (s : ℝ) (hQ : Q.scale = 0) : coarseCaccioppoliBufferedCrossBudget Q s (fullVectorPoincareCubeConstant Q) = coarseCaccioppoliBufferedCrossBudgetUnit d s

theorem HCPolySupport.coarseCaccioppoliBufferedBudgetSplit_spec {d : ℕ} [NeZero d] (Q : TriadicCube d) (s t Csol : ℝ) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) : Csol ≤ coarseCaccioppoliBufferedLocalBudget Q Csol ∧ 0 ≤ coarseCaccioppoliBufferedLocalBudget Q Csol ∧ 0 < coarseCaccioppoliBufferedAlphaBudget Q s Csol ∧ 0 ≤ coarseCaccioppoliBufferedCrossBudget Q s Csol ∧ 81 * Real.rpow 3 s * (↑(Fintype.card (Fin d)) * coarseCaccioppoliBufferedLocalBudget Q Csol) ≤ ↑(Fintype.card (Fin d)) * coarseCaccioppoliBufferedCrossBudget Q s Csol ∧ 81 * (2 * coarseCaccioppoliCenteredAverageFront d s (↑(Fintype.card (Fin d)) * coarseCaccioppoliBufferedLocalBudget Q Csol) + 4 * coarseCaccioppoliCenteredBesovHessianFront d s (↑(Fintype.card (Fin d)) * coarseCaccioppoliBufferedLocalBudget Q Csol) + 2 * coarseCaccioppoliCenteredBesovGradientFront d s (↑(Fintype.card (Fin d)) * coarseCaccioppoliBufferedLocalBudget Q Csol)) ≤ ↑(Fintype.card (Fin d)) * coarseCaccioppoliBufferedAlphaBudget Q s Csol / (s * (1 - s)) ∧ coarseCaccioppoliBufferedCutoffBudget Q ≤ ↑(Fintype.card (Fin d)) * coarseCaccioppoliBufferedLocalBudget Q Csol

The explicit split centered buffered budgets satisfy the scalar side conditions needed by the split exact raw-coefficient package.

theorem HCPolySupport.coarseCaccioppoli_boundary_qone_standard_note_of_of_closedCubeEllipticity {d : ℕ} [NeZero d] (Q : TriadicCube d) (center : Vec d) (a : CoeffField d) (s t : ℝ) {lam Lam : ℝ} (u : AHarmonicFunction a (openCubeSet Q)) (hzero : LocalizedZeroTraceFunctionOn (openCubeSet Q) (coarseCaccioppoliLocalOpenCube Q center 1) u.toH1.toFun) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) : have Csol := fullVectorPoincareCubeConstant Q; have Calpha := coarseCaccioppoliLocalPatchBufferedAlphaBudget Q s Csol; have Ccross := coarseCaccioppoliLocalPatchBufferedCrossBudget Q s Csol; have Cnote := coarseCaccioppoliBoundaryStandardExplicitNoteConstantSplit Q a s t (↑(Fintype.card (Fin d)) * Calpha) (↑(Fintype.card (Fin d)) * Ccross); 0 ≤ Cnote ∧ coarseCaccioppoliLocalEnergyRadiusProfile Q center (fun (x : Vec d) => scalarVariationEnergyIntegrand a u x) (1 / 3) ≤ coarseCaccioppoliBoundaryNoteRhs Q a s t Cnote (coarseCaccioppoliHarmonicL2Sq Q a u)

Boundary local-patch Caccioppoli with explicit split max-chosen budgets, using the standard beta-dependent radius iteration.

This is the repaired arbitrary-center boundary endpoint: the deterministic bridge is all-radii, and the note constant is the standard split one.

theorem HCPolySupport.coarseCaccioppoli_boundary_qone_standard_note_of_closedCubeEllipticity {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s t : ℝ) {lam Lam : ℝ} (u : AHarmonicFunction a (openCubeSet Q)) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) : have Csol := fullVectorPoincareCubeConstant Q; have Calpha := coarseCaccioppoliBufferedAlphaBudget Q s Csol; have Ccross := coarseCaccioppoliBufferedCrossBudget Q s Csol; have Cnote := coarseCaccioppoliBoundaryStandardExplicitNoteConstantSplit Q a s t (↑(Fintype.card (Fin d)) * Calpha) (↑(Fintype.card (Fin d)) * Ccross); 0 ≤ Cnote ∧ coarseCaccioppoliLocalizedEnergyRadiusProfile Q (fun (x : Vec d) => scalarVariationEnergyIntegrand a u x) (1 / 3) ≤ coarseCaccioppoliBoundaryNoteRhs Q a s t Cnote (coarseCaccioppoliHarmonicL2Sq Q a u)

Boundary centered Caccioppoli with explicit split budgets and the standard beta-dependent radius iteration.

This is the m = 0 centered note-RHS endpoint with all all-radii coefficient and raw-bridge inputs constructed internally.

theorem HCPolySupport.coarseCaccioppoli_interior_qone_standard_note_of_closedCubeEllipticity {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s t : ℝ) {lam Lam : ℝ} (u : AHarmonicFunction a (openCubeSet Q)) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) : have Csol := fullVectorPoincareCubeConstant Q; have Calpha := coarseCaccioppoliBufferedAlphaBudget Q s Csol; have Ccross := coarseCaccioppoliBufferedCrossBudget Q s Csol; have Cnote := coarseCaccioppoliBoundaryStandardExplicitNoteConstantSplit Q a s t (↑(Fintype.card (Fin d)) * Calpha) (↑(Fintype.card (Fin d)) * Ccross); 0 ≤ Cnote ∧ coarseCaccioppoliLocalizedEnergyRadiusProfile Q (fun (x : Vec d) => scalarVariationEnergyIntegrand a u x) (1 / 3) ≤ coarseCaccioppoliInteriorNoteRhs Q a s t Cnote (coarseCaccioppoliHarmonicL2Sq Q a u)

Interior centered Caccioppoli with explicit split budgets and the standard beta-dependent radius iteration.