Coarse-graining support: Support.Deterministic.CoarseCaccioppoli.EnergyBridge.CutoffSizes

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

noncomputable def HCPolySupport.coarseCaccioppoliConstantCutoffSize {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (ξ : Vec d → Vec d) (B : ℝ) : ℝ

Exact cutoff size controlling the constant piece (u)_Q ξ.

The local split theorem only needs this quantity through an upper bound, but keeping the exact expression here gives the next coefficient-bookkeeping layer a stable target to dominate by the note's radius/height constants.

Equations

• HCPolySupport.coarseCaccioppoliConstantCutoffSize Q u ξ B = HCPolySupport.cubeLpNorm Q 2 u * (B + HCPolySupport.cubeBesovScaleWeight 1 Q * HCPolySupport.cubeLpNorm Q ⊤ ξ)

noncomputable def HCPolySupport.coarseCaccioppoliCenteredCutoffSize {d : ℕ} (Q : TriadicCube d) (s : ℝ) (ξ : Vec d → Vec d) (Acirc1 AcircS E B C : ℝ) : ℝ

Exact cutoff size controlling the centered piece (u-(u)_Q) ξ after the cutoff-product theorem and projected mean-zero Poincare estimate have supplied the two scalar circ bounds.

Equations

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

theorem HCPolySupport.coarseCaccioppoliConstantCutoffSize_nonneg {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (ξ : Vec d → Vec d) {B : ℝ} (hB : 0 ≤ B) : 0 ≤ coarseCaccioppoliConstantCutoffSize Q u ξ B

theorem HCPolySupport.coarseCaccioppoliConstantCutoffSize_pos_of_cubeLpNorm_pos_of_B_pos {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (ξ : Vec d → Vec d) {B : ℝ} (hu : 0 < cubeLpNorm Q 2 u) (hB : 0 < B) : 0 < coarseCaccioppoliConstantCutoffSize Q u ξ B

noncomputable def HCPolySupport.coarseCaccioppoliConstantCutoffSizeFactorBound {d : ℕ} (Q : TriadicCube d) (U Xi D : ℝ) : ℝ

Separated upper bound for the constant cutoff size. In applications U is a note-facing bound for ‖u‖_{L^2(Q)} and Xi, D bound the cutoff and its derivative.

Equations

• HCPolySupport.coarseCaccioppoliConstantCutoffSizeFactorBound Q U Xi D = U * (D + HCPolySupport.cubeBesovScaleWeight 1 Q * Xi)

theorem HCPolySupport.coarseCaccioppoliConstantCutoffSizeFactorBound_nonneg {d : ℕ} (Q : TriadicCube d) {U Xi D : ℝ} (hU : 0 ≤ U) (hXi : 0 ≤ Xi) (hD : 0 ≤ D) : 0 ≤ coarseCaccioppoliConstantCutoffSizeFactorBound Q U Xi D

theorem HCPolySupport.coarseCaccioppoliConstantCutoffSize_le_factorBound {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (ξ : Vec d → Vec d) {B U Xi D : ℝ} (hU_nonneg : 0 ≤ U) (hB_nonneg : 0 ≤ B) (hu : cubeLpNorm Q 2 u ≤ U) (hξ : cubeLpNorm Q ⊤ ξ ≤ Xi) (hB : B ≤ D) : coarseCaccioppoliConstantCutoffSize Q u ξ B ≤ coarseCaccioppoliConstantCutoffSizeFactorBound Q U Xi D

theorem HCPolySupport.coarseCaccioppoliCenteredCutoffSize_nonneg {d : ℕ} (Q : TriadicCube d) {s : ℝ} (ξ : Vec d → Vec d) {Acirc1 AcircS E B C : ℝ} (hs : 0 < s) (hAcirc1 : 0 ≤ Acirc1) (hAcircS : 0 ≤ AcircS) (hE : 0 ≤ E) (hB : 0 ≤ B) (hC : 0 ≤ C) : 0 ≤ coarseCaccioppoliCenteredCutoffSize Q s ξ Acirc1 AcircS E B C

theorem HCPolySupport.coarseCaccioppoliCenteredCutoffSize_pos_of_first_branch {d : ℕ} (Q : TriadicCube d) {s : ℝ} (ξ : Vec d → Vec d) {Acirc1 AcircS E B C : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (hAcirc1 : 0 < Acirc1) (hAcircS : 0 ≤ AcircS) (hE : 0 < E) (hB : 0 < B) (hC : 0 < C) : 0 < coarseCaccioppoliCenteredCutoffSize Q s ξ Acirc1 AcircS E B C

def HCPolySupport.CoarseCaccioppoliFluxEnergyControls {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (flux : Vec d → Vec d) (energy : Vec d → ℝ) : Prop

Flux-side hypotheses needed to substitute coarse-Poincare energy controls into the local Caccioppoli split theorem.

Equations

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

theorem HCPolySupport.CubeAverageGradientEnergyControl.restrict_to_descendant {d : ℕ} {Q R : TriadicCube d} {j : ℕ} {a : CoeffField d} {g : Vec d → Vec d} {energy : Vec d → ℝ} (hgrad : CubeAverageGradientEnergyControl Q a g energy) (hR : R ∈ descendantsAtDepth Q j) : CubeAverageGradientEnergyControl R a g energy

Gradient-average energy controls restrict from a parent cube to any depth-j descendant.

theorem HCPolySupport.CoarseCaccioppoliFluxEnergyControls.restrict_to_descendant {d : ℕ} {Q R : TriadicCube d} {j : ℕ} {a : CoeffField d} {s : ℝ} {flux : Vec d → Vec d} {energy : Vec d → ℝ} (hctrl : CoarseCaccioppoliFluxEnergyControls Q a s flux energy) (hs : 0 ≤ s) (hR : R ∈ descendantsAtDepth Q j) : CoarseCaccioppoliFluxEnergyControls R a s flux energy

Flux-energy controls restrict from a parent cube to any depth-j descendant.

theorem HCPolySupport.CoarseCaccioppoliFluxEnergyControls.of_aHarmonicFunction_of_isEllipticFieldOn {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) {lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (u : AHarmonicFunction a (cubeSet Q)) : CoarseCaccioppoliFluxEnergyControls Q a s (fun (x : Vec d) => matVecMul (a x) (u.toH1.grad x)) fun (x : Vec d) => scalarVariationEnergyIntegrand a u x

Harmonic closed-cube constructor for the flux energy-control package used by the Caccioppoli bridge. The final note-facing endpoints still work on open cubes; this lemma records the exact stronger compatibility hypothesis under which the flux package is already available from the coarse-Poincare API.

def HCPolySupport.CoarseCaccioppoliScalarCutoffControls {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → ℝ) (ξ : Vec d → Vec d) (energy : Vec d → ℝ) (Acirc1 AcircS B C : ℝ) : Prop

Scalar projected-Poincare and cutoff-product hypotheses remaining after the flux-side coarse-Poincare controls have been substituted.

Equations

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

def HCPolySupport.CoarseCaccioppoliVectorCutoffControls {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → ℝ) (G ξ : Vec d → Vec d) (energy : Vec d → ℝ) (Acirc1 AcircS B C : ℝ) : Prop

Vector projected-Poincare and cutoff-product hypotheses remaining after the flux-side coarse-Poincare controls have been substituted.

The Poincare constant is the vector constant C; downstream exact RHS bookkeeping uses the effective scalar-shaped constant (Fintype.card (Fin d) : ℝ) * C, reflecting the sum over gradient components.

Equations

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