Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.EnergyBridge.LocalEstimate.SingleCube

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

Local energy estimate: single-cube note RHS bridge

theorem HCPolySupport.abs_cubeAverage_vecDot_scalar_smul_le_singleCubeBoundaryNoteRhs_of_controls {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 k h uL2Sq : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (hfluxMem : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q)) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hg : 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) (hdom : CoarseCaccioppoliSingleCubeCoefficientDomination Q a s C k h uL2Sq u ξ energy Acirc1 AcircS B) : |cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ coarseCaccioppoliSingleCubeBoundaryNoteRhs Q a s C k h uL2Sq (cubeAverage Q energy)

Note single-cube estimate obtained from the exact local bridge once the remaining coefficient-domination obligation has been supplied.

theorem HCPolySupport.abs_cubeAverage_vecDot_scalar_smul_le_singleCubeBoundaryNoteRhs_of_vectorControls {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 k h uL2Sq : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (hfluxMem : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q)) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hG : ∀ (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) (hdom : CoarseCaccioppoliSingleCubeCoefficientDomination Q a s (↑(Fintype.card (Fin d)) * C) k h uL2Sq u ξ energy Acirc1 AcircS B) : |cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ coarseCaccioppoliSingleCubeBoundaryNoteRhs Q a s (↑(Fintype.card (Fin d)) * C) k h uL2Sq (cubeAverage Q energy)

Note single-cube estimate from the vector projected-Poincare package and a coefficient-domination proof stated for the effective scalar-facing constant (Fintype.card (Fin d) : ℝ) * C.

theorem HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_singleCubeBoundaryNoteRhs {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (a : CoeffField d) (s : ℝ) {ρ₁ ρ₂ : ℝ} (flux : Vec d → Vec d) (u : Vec d → ℝ) (G : Vec d → Vec d) (energy : Vec d → ℝ) (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) {Acirc1 AcircS C k h uL2Sq : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (hfluxMem : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure R)) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure R)) (hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure R)) (hfluxEnergy : CoarseCaccioppoliFluxEnergyControls R a s flux energy) (hB : 0 ≤ quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2) (hAcircS : 0 ≤ AcircS) (hBgConst : 0 ≤ coarseCaccioppoliConstantCutoffSize R u (scalarCutoffGradientField η.toFun) (quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2)) (hBgCent : 0 ≤ coarseCaccioppoliCenteredCutoffSize R s (scalarCutoffGradientField η.toFun) Acirc1 AcircS (√(cubeAverage R energy)) (quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2) (↑(Fintype.card (Fin d)) * C)) (hC : 0 ≤ C) (hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate R C (cubeFluctuation R u) G N) (hGcirc1 : ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm R 1 2 1 N fun (x : Vec d) => G x i) ≤ Acirc1 * √(cubeAverage R energy)) (hGcircS : ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm R (1 - s) 2 1 N fun (x : Vec d) => G x i) ≤ AcircS * √(cubeAverage R energy)) (hdom : CoarseCaccioppoliSingleCubeCoefficientDomination R a s (↑(Fintype.card (Fin d)) * C) k h uL2Sq u (scalarCutoffGradientField η.toFun) energy Acirc1 AcircS (quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2)) : |cubeAverage R fun (x : Vec d) => vecDot (flux x) (u x • scalarCutoffGradientField η.toFun x)| ≤ coarseCaccioppoliSingleCubeBoundaryNoteRhs R a s (↑(Fintype.card (Fin d)) * C) k h uL2Sq (cubeAverage R energy)

Note single-cube estimate on a descendant cube using a parent quantitative cutoff, after the small-cube coefficient domination has been supplied.

theorem HCPolySupport.abs_cubeAverage_vecDot_scalar_smul_le_singleCubeBoundaryNoteRhs_of_coefficientControls {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 k h uL2Sq : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (hfluxMem : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q)) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hg : 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) (hcoeff : CoarseCaccioppoliSingleCubeCoefficientControls Q a s C k h uL2Sq u ξ Acirc1 AcircS B) : |cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ coarseCaccioppoliSingleCubeBoundaryNoteRhs Q a s C k h uL2Sq (cubeAverage Q energy)

Note single-cube estimate obtained directly from the factored coefficient controls. The nonnegativity of the averaged energy is supplied by the flux-energy bundle, so callers only need the two scalar coefficient inequalities.

theorem HCPolySupport.abs_cubeAverage_vecDot_scalar_smul_le_singleCubeBoundaryNoteRhs_of_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 k h uL2Sq A G X Y : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (hfluxMem : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q)) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hg : 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) (hA_nonneg : 0 ≤ A) (hconstCoeff : coarseCaccioppoliFluxEnergyExactConstantCoeff Q a ≤ A) (hconstCutoff : coarseCaccioppoliConstantCutoffSize Q u ξ B ≤ G) (hconst : A * G ≤ coarseCaccioppoliSingleCubeBoundaryConstantCoeff Q a C k uL2Sq) (havg : coarseCaccioppoliFluxEnergyExactCenteredAverageCoeff Q a ξ Acirc1 C ≤ X) (hbesov : coarseCaccioppoliFluxEnergyExactCenteredBesovCoeff Q a s ξ Acirc1 AcircS B C ≤ Y) (hcentered : X + Y ≤ coarseCaccioppoliSingleCubeBoundaryCenteredCoeff Q a s C k h) : |cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ coarseCaccioppoliSingleCubeBoundaryNoteRhs Q a s C k h uL2Sq (cubeAverage Q energy)

Note single-cube estimate from the most separated coefficient inputs: a constant coefficient bound, a constant cutoff-size bound, and termwise centered average/Besov bounds.

theorem HCPolySupport.abs_cubeAverage_vecDot_scalar_smul_le_singleCubeBoundaryNoteRhs_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 k h uL2Sq U Xi D A1 AS : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (hfluxMem : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q)) (huMem : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hg : 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 ≤ coarseCaccioppoliSingleCubeBoundaryConstantCoeff Q a C k uL2Sq) (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) ≤ coarseCaccioppoliSingleCubeBoundaryCenteredCoeff Q a s C k h) : |cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ coarseCaccioppoliSingleCubeBoundaryNoteRhs Q a s C k h uL2Sq (cubeAverage Q energy)

Note single-cube estimate from canonical coefficient factors and primitive scalar cutoff bounds. This is the fixed-cube counterpart of the canonical radius-energy input in CoarseCaccioppoliSingleCubeToRaw.