Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.RadiusInputs.Profiles

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

theorem HCPolySupport.abs_cubeAverage_vecDot_scalar_smul_le_boundaryRawEstimate_of_canonical_vector_factor_bounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (flux : Vec d → Vec d) (u : Vec d → ℝ) (G ξ : 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 : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) (hfluxEnergy : CoarseCaccioppoliFluxEnergyControls Q a s flux energy) (hvector : CoarseCaccioppoliVectorCutoffControls 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 (↑(Fintype.card (Fin d)) * C) + coarseCaccioppoliFluxEnergyExactCenteredBesovCoeffFactorBound Q s (coarseCaccioppoliLambdaFactor Q a s) (coarseCaccioppoliLambdaFactor Q a s) (coarseCaccioppoliCenteredCutoffCoeffFactorBound Q s Xi D A1 AS (↑(Fintype.card (Fin d)) * C)) ≤ Alpha) : |cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ Alpha * cubeAverage Q energy + Bcross * √(cubeAverage Q energy)

Single-pair raw boundary estimate from the vector projected-Poincare cutoff package and canonical coefficient factor bounds. The raw coefficients are evaluated at the effective scalar-facing constant (Fintype.card (Fin d) : ℝ) * C.

theorem HCPolySupport.coarseCaccioppoli_boundary_noteEstimate_of_rawCoefficientBounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (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 : ℝ → ℝ → ℝ) (hs0 : 0 < s) (hs1 : s < 1) (hanalytic : CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalVectorAnalyticInputs 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 (↑(Fintype.card (Fin d)) * C) uL2Sq h U Xi D A1 AS) : CoarseCaccioppoliBoundaryNoteRawEstimate Q a s t (↑(Fintype.card (Fin d)) * C) uL2Sq h F

Vector-Poincare raw boundary estimate from the radius-indexed analytic package and raw coefficient bounds stated with the effective scalar-facing constant (Fintype.card (Fin d) : ℝ) * C.

theorem HCPolySupport.coarseCaccioppoli_boundary_singleCubeEstimate_of_coefficientBounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C uL2Sq : ℝ) (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 : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs0 : 0 < s) (hs1 : s < 1) (hanalytic : CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalVectorAnalyticInputs Q a s C k h F flux u G ξ energy Acirc1 AcircS B U Xi D A1 AS) (hcoeff : CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalCoefficientBounds Q a s (↑(Fintype.card (Fin d)) * C) uL2Sq k h U Xi D A1 AS) : CoarseCaccioppoliBoundarySingleCubeRawEstimate Q a s (↑(Fintype.card (Fin d)) * C) uL2Sq k h F

Vector-Poincare single-cube estimate from the radius-indexed analytic package and the note-shaped single-cube coefficient bounds. The local vector Poincare constant is C; the scalar-facing single-cube RHS uses the effective constant (Fintype.card (Fin d) : ℝ) * C.

theorem HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs.of_factorInputs {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 : ℝ → ℝ → ℝ) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeFactorInputs Q a s C uL2Sq k h F flux u g ξ energy Acirc1 AcircS B A G X Y) : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq k h F flux u g ξ energy Acirc1 AcircS B

theorem HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs.of_separatedFactorInputs {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 : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs0 : 0 < s) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeSeparatedFactorInputs Q a s C uL2Sq k h F flux u g ξ energy Acirc1 AcircS B AavgConst AavgCent Aflux1 AfluxS U Xi D A1 AS) : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq k h F flux u g ξ energy Acirc1 AcircS B

theorem HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeSeparatedFactorInputs.of_canonicalFactorInputs {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 : ℝ → ℝ → ℝ) (hs0 : 0 < s) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalFactorInputs Q a s C uL2Sq k h F flux u g ξ energy Acirc1 AcircS B U Xi D A1 AS) : CoarseCaccioppoliBoundaryRadiusEnergyBridgeSeparatedFactorInputs Q a s C uL2Sq k h F flux u g ξ energy Acirc1 AcircS B (fun (x x_1 : ℝ) => coarseCaccioppoliLambdaFactor Q a 1) (fun (x x_1 : ℝ) => coarseCaccioppoliLambdaFactor Q a s) (fun (x x_1 : ℝ) => coarseCaccioppoliLambdaFactor Q a 1) (fun (x x_1 : ℝ) => coarseCaccioppoliLambdaFactor Q a s) U Xi D A1 AS

theorem HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs.of_canonicalFactorInputs {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 : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs0 : 0 < s) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalFactorInputs Q a s C uL2Sq k h F flux u g ξ energy Acirc1 AcircS B U Xi D A1 AS) : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq k h F flux u g ξ energy Acirc1 AcircS B

theorem HCPolySupport.coarseCaccioppoli_boundary_singleCubeRawEstimate_of_radiusEnergyBridgeInputs {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 : ℝ → ℝ → ℝ) (hs0 : 0 < s) (hs1 : s < 1) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq k h F flux u g ξ energy Acirc1 AcircS B) : CoarseCaccioppoliBoundarySingleCubeRawEstimate Q a s C uL2Sq k h F

theorem HCPolySupport.coarseCaccioppoli_boundary_singleCubeRawEstimate_of_radiusEnergyBridgeFactorInputs {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 : ℝ → ℝ → ℝ) (hs0 : 0 < s) (hs1 : s < 1) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeFactorInputs Q a s C uL2Sq k h F flux u g ξ energy Acirc1 AcircS B A G X Y) : CoarseCaccioppoliBoundarySingleCubeRawEstimate Q a s C uL2Sq k h F

Radius-indexed factor inputs produce the note-facing single-cube raw estimate after assembling the bundled coefficient controls.

theorem HCPolySupport.coarseCaccioppoli_boundary_singleCubeRawEstimate_of_radiusEnergyBridgeSeparatedFactorInputs {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 : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs0 : 0 < s) (hs1 : s < 1) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeSeparatedFactorInputs Q a s C uL2Sq k h F flux u g ξ energy Acirc1 AcircS B AavgConst AavgCent Aflux1 AfluxS U Xi D A1 AS) : CoarseCaccioppoliBoundarySingleCubeRawEstimate Q a s C uL2Sq k h F

Radius-indexed primitive separated factor inputs produce the note-facing single-cube raw estimate.

theorem HCPolySupport.coarseCaccioppoli_boundary_singleCubeRawEstimate_of_radiusEnergyBridgeCanonicalFactorInputs {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 : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs0 : 0 < s) (hs1 : s < 1) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalFactorInputs Q a s C uL2Sq k h F flux u g ξ energy Acirc1 AcircS B U Xi D A1 AS) : CoarseCaccioppoliBoundarySingleCubeRawEstimate Q a s C uL2Sq k h F

Radius-indexed canonical factor inputs produce the note-facing single-cube raw estimate.