Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.RadiusInputs.Setup

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

def HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) (F : ℝ → ℝ) (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B : ℝ → ℝ → ℝ) : Prop

Radius-indexed local data sufficient for the energy bridge to produce the single-cube note estimate at every radius pair. This packages the testing inequality, L^p hypotheses, flux-energy controls, scalar cutoff controls, and the two exact local coefficient inequalities.

Equations

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

def HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeFactorInputs {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) (F : ℝ → ℝ) (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B A G X Y : ℝ → ℝ → ℝ) : Prop

Radius-indexed energy bridge inputs with the final coefficient comparison kept in the separated factor form supplied by CoarseCaccioppoliSingleCubeCoefficientControls.of_factor_bounds.

Equations

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

def HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeSeparatedFactorInputs {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) (F : ℝ → ℝ) (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B AavgConst AavgCent Aflux1 AfluxS U Xi D A1 AS : ℝ → ℝ → ℝ) : Prop

Radius-indexed energy bridge inputs with the coefficient comparison stated in primitive separated scalar factors. This is the closest current interface to a concrete cutoff construction: callers provide bounds for ‖u‖₂, ‖ξ‖∞, ‖∇ξ‖∞, the two scalar projected-Poincare factors, and the three coefficient factors.

Equations

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

def HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalFactorInputs {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) (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 : ℝ → ℝ → ℝ) : Prop

Radius-indexed energy bridge inputs with the coefficient factors fixed to the canonical LambdaSq choices. This removes the four average/flux coefficient slots from the caller-facing local interface; the bounds for those slots are recovered from the flux-energy summability hypotheses.

Equations

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

def HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalAnalyticInputs {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C : ℝ) (_k _h : ℝ → ℝ → ℝ) (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 : ℝ → ℝ → ℝ) : Prop

Analytic/local part of the canonical radius-indexed energy bridge inputs. This deliberately omits the final two single-cube coefficient inequalities: those are separated below so an actual cutoff construction can first prove the testing, integrability, flux-energy, scalar-cutoff, and primitive scalar bounds without also carrying the coefficient-localization algebra.

Equations

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

def HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalVectorAnalyticInputs {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C : ℝ) (_k _h : ℝ → ℝ → ℝ) (F : ℝ → ℝ) (flux : ℝ → ℝ → Vec d → Vec d) (u : ℝ → ℝ → Vec d → ℝ) (G ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B U Xi D A1 AS : ℝ → ℝ → ℝ) : Prop

Vector-Poincare version of CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalAnalyticInputs.

The local cutoff package uses a vector Poincare constant C; downstream coefficient and height bounds are stated with the effective scalar-facing constant (Fintype.card (Fin d) : ℝ) * C.

Equations

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

def HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalCoefficientBounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C uL2Sq : ℝ) (k h U Xi D A1 AS : ℝ → ℝ → ℝ) : Prop

The two radius-indexed coefficient inequalities left after the canonical local analytic inputs have been supplied. This is the formal target for the Chapter 3 cutoff-scale algebra: constant branch and centered branch.

Equations

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

def HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalRawCoefficientBounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (h U Xi D A1 AS : ℝ → ℝ → ℝ) : Prop

Direct radius-indexed comparison from the canonical factor bounds to the final boundary raw coefficients. This is the natural top-level bookkeeping surface once the local estimate is targeted straight at the note's raw radius recursion rather than routed through the intermediate single-cube coefficients.

Equations

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

theorem HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalRawCoefficientBounds.of_coefficientBounds_of_localization {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k h U Xi D A1 AS : ℝ → ℝ → ℝ) (hcoeff : CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalCoefficientBounds Q a s C uL2Sq k h U Xi D A1 AS) (hloc : CoarseCaccioppoliBoundarySingleCubeCoefficientLocalization Q a s t C uL2Sq k h) : CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalRawCoefficientBounds Q a s t C uL2Sq h U Xi D A1 AS

theorem HCPolySupport.abs_cubeAverage_vecDot_scalar_smul_le_boundaryRawEstimate_of_canonical_factor_bounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (flux : Vec d → Vec d) (u g : Vec d → ℝ) (ξ : Vec d → Vec d) (energy : Vec d → ℝ) {Acirc1 AcircS B C U Xi D A1 AS Alpha Bcross : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (hfluxMem : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q)) (huMem : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hgMem : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) (hfluxEnergy : CoarseCaccioppoliFluxEnergyControls Q a s flux energy) (hscalar : CoarseCaccioppoliScalarCutoffControls Q s u g ξ energy Acirc1 AcircS B C) (hAcirc1_nonneg : 0 ≤ Acirc1) (hAcircS_nonneg : 0 ≤ AcircS) (hu : cubeLpNorm Q 2 u ≤ U) (hξ : cubeLpNorm Q ⊤ ξ ≤ Xi) (hB : B ≤ D) (hAcirc1 : Acirc1 ≤ A1) (hAcircS : AcircS ≤ AS) (hconst : coarseCaccioppoliFluxEnergyExactConstantCoeffFactorBound Q (coarseCaccioppoliLambdaFactor Q a 1) (coarseCaccioppoliLambdaFactor Q a 1) * coarseCaccioppoliConstantCutoffSizeFactorBound Q U Xi D ≤ Bcross) (hcentered : coarseCaccioppoliFluxEnergyExactCenteredAverageCoeffFactorBound (coarseCaccioppoliLambdaFactor Q a s) Xi A1 C + coarseCaccioppoliFluxEnergyExactCenteredBesovCoeffFactorBound Q s (coarseCaccioppoliLambdaFactor Q a s) (coarseCaccioppoliLambdaFactor Q a s) (coarseCaccioppoliCenteredCutoffCoeffFactorBound Q s Xi D A1 AS C) ≤ Alpha) : |cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ Alpha * cubeAverage Q energy + Bcross * √(cubeAverage Q energy)

theorem HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalFactorInputs.of_analytic_inputs_bounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) (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 : ℝ → ℝ → ℝ) (hanalytic : CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalAnalyticInputs Q a s C k h F flux u g ξ energy Acirc1 AcircS B U Xi D A1 AS) (hcoeff : CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalCoefficientBounds Q a s C uL2Sq k h U Xi D A1 AS) : CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalFactorInputs Q a s C uL2Sq k h F flux u g ξ energy Acirc1 AcircS B U Xi D A1 AS

theorem HCPolySupport.coarseCaccioppoli_boundary_noteEstimate_of_radiusEnergyAnalyticInputs {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) {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 : ℝ → ℝ → ℝ) (hs0 : 0 < s) (hs1 : s < 1) (hanalytic : CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalAnalyticInputs Q a s C (fun (x x_1 : ℝ) => 0) h F flux u g ξ energy Acirc1 AcircS B U Xi D A1 AS) (hcoeff : CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalRawCoefficientBounds Q a s t C uL2Sq h U Xi D A1 AS) : CoarseCaccioppoliBoundaryNoteRawEstimate Q a s t C uL2Sq h F