Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicFinal.Setup.CoefficientBounds

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

Final-facing canonical harmonic Caccioppoli endpoints

This file keeps the last public theorem surface readable. The coefficient algebra is still a real remaining hypothesis, but it is now exposed as one named Chapter-3 schedule rather than as the full expanded U/Xi/D/A1/AS expression at every endpoint.

def HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicCoefficientBounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)) : Prop

The exact coefficient-schedule hypothesis left for the fully canonical harmonic-gradient Caccioppoli endpoint.

It specializes the generic canonical coefficient bounds to the Chapter-3 triadic gap scale, the localized explicit height, the harmonic L² profile, the canonical quantitative cutoff bounds, and the canonical gradient Acirc factors.

Equations

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

def HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicRawCoefficientBounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)) : Prop

The same fully canonical harmonic coefficient schedule after the single-cube coefficient bounds have already been localized to the raw radius recursion coefficients Alpha and Bcross.

This is the natural handoff point for the concrete cutoff construction: prove the two raw inequalities once, then invoke the final Caccioppoli wrapper without also carrying the multiscale localization data.

Equations

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

def HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicL2SizeControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (uL2Sq : ℝ) (w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)) : Prop

Note-facing L² size control for the harmonic family.

The scalar uL2Sq is the squared L² size appearing in the public RHS. This package is the honest public replacement for the U component hidden inside the coefficient-schedule hypothesis: every radius-pair harmonic function has normalized L² norm bounded by sqrt uL2Sq.

Equations

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

noncomputable def HCPolySupport.coarseCaccioppoliHarmonicL2Sq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : AHarmonicFunction a (openCubeSet Q)) : ℝ

The actual squared normalized L² size of a single open-cube harmonic function, in the units used by the public note RHS.

Equations

• HCPolySupport.coarseCaccioppoliHarmonicL2Sq Q a u = (HCPolySupport.cubeLpNorm Q 2 fun (x : HCPolySupport.Vec d) => u.toH1.toFun x) ^ 2

theorem HCPolySupport.coarseCaccioppoliHarmonicL2Sq_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : AHarmonicFunction a (openCubeSet Q)) : 0 ≤ coarseCaccioppoliHarmonicL2Sq Q a u

theorem HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicL2SizeControl.of_constantFamily {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : AHarmonicFunction a (openCubeSet Q)) : CoarseCaccioppoliBoundaryCanonicalHarmonicL2SizeControl Q a (coarseCaccioppoliHarmonicL2Sq Q a u) fun (x x_1 : ℝ) => u

The constant harmonic family has the note-facing L² size control with the actual squared normalized L² size.