Coarse-graining support: #
Support.Deterministic.CoarseCaccioppoli.EnergyBridge.LocalEstimateFullDual
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Full-dual local Caccioppoli estimate #
This sidecar is the corrected full-dual/local-multiscale analogue of the
vector projected-Poincare local estimate in LocalEstimate.lean.
theorem
HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_split_of_fluxEnergyControl_of_vector
{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 BgConst BgCent : ℝ}
(hB : 0 ≤ B)
(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))
(hBgConst : 0 ≤ BgConst)
(hBgCent : 0 ≤ BgCent)
(hC : 0 ≤ C)
(hAcirc1 : 0 ≤ Acirc1)
(hAcircS : 0 ≤ AcircS)
(henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x)
(henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume)
(hfluxCtrl : CubeAverageFluxEnergyControl Q a flux energy)
(hsum1 :
Summable fun (n : ℕ) => geometricWeight 1 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hsumS :
Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hfull : ∀ (N : ℕ), CubeDescendantDualFullVectorPoincareEstimate Q C (cubeFluctuation Q u) G N)
(hlocal : ∀ (N : ℕ), CubeLocalMultiscalePoincareVectorEstimate Q (3 / 2 * C * 3 ^ (↑d + 1)) (cubeFluctuation Q u) G N)
(hξ : ∀ (i : Fin d), ContDiff ℝ ↑⊤ fun (x : Vec d) => ξ x i)
(hderiv : ∀ (i : Fin d), ∀ z ∈ cubeSet Q, ‖fderiv ℝ (fun (x : Vec d) => ξ x i) z‖ ≤ B)
(hGcirc1 :
∀ (i : Fin d) (N : ℕ),
(cubeBesovCircPartialNorm Q 1 2 1 N fun (x : Vec d) => G x i) ≤ Acirc1 * √(cubeAverage Q energy))
(hGcircS :
∀ (i : Fin d) (N : ℕ),
(cubeBesovCircPartialNorm Q (1 - s) 2 1 N fun (x : Vec d) => G x i) ≤ AcircS * √(cubeAverage Q energy))
(hBgConst_bound : cubeLpNorm Q 2 u * (B + cubeBesovScaleWeight 1 Q * cubeLpNorm Q ⊤ ξ) ≤ BgConst)
(hBgCent_bound :
2 * (cubeScaleFactor Q * B * (√(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * (3 / 2 * (↑(Fintype.card (Fin d)) * C) * 3 ^ (↑d + 1) * (Acirc1 * √(cubeAverage Q energy)))) + cubeLpNorm Q ⊤ ξ * (cubeBesovScaleWeight (-s) Q * (3 / 2 * (↑(Fintype.card (Fin d)) * C) * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * (AcircS * √(cubeAverage Q energy))))) ≤ BgCent)
:
have E := √(cubeAverage Q energy);
have Aavg := √(coarseBBlockNorm Q a);
have Aflux1 := (geometricDiscount 1 1)⁻¹ * (LambdaSq Q 1 (MultiscaleExponent.finite 1) a).rpow (1 / 2);
have AfluxS := (geometricDiscount s 1)⁻¹ * (LambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (1 / 2);
|cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ ↑d * (3 ^ (↑d + 1) * (cubeBesovScaleWeight (-1) Q * (Aflux1 * E)) * BgConst) + (↑d * (Aavg * E * (cubeLpNorm Q ⊤ ξ * (3 / 2 * (↑(Fintype.card (Fin d)) * C) * 3 ^ (↑d + 1) * (Acirc1 * E)))) + ↑d * (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * (AfluxS * E)) * (cubeBesovScaleWeight s Q * BgCent)))
theorem
HCPolySupport.abs_cubeAverage_vecDot_scalar_smul_le_fluxEnergyExactRhs_of_vectorFullDualLocalMultiscale
{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 : ℝ}
(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)
(hB : 0 ≤ B)
(hAcirc1 : 0 ≤ Acirc1)
(hAcircS : 0 ≤ AcircS)
(hBgConst : 0 ≤ coarseCaccioppoliConstantCutoffSize Q u ξ B)
(hBgCent :
0 ≤ coarseCaccioppoliCenteredCutoffSize Q s ξ Acirc1 AcircS (√(cubeAverage Q energy)) B (↑(Fintype.card (Fin d)) * C))
(hC : 0 ≤ C)
(hfull : ∀ (N : ℕ), CubeDescendantDualFullVectorPoincareEstimate Q C (cubeFluctuation Q u) G N)
(hlocal : ∀ (N : ℕ), CubeLocalMultiscalePoincareVectorEstimate Q (3 / 2 * C * 3 ^ (↑d + 1)) (cubeFluctuation Q u) G N)
(hξ : ∀ (i : Fin d), ContDiff ℝ ↑⊤ fun (x : Vec d) => ξ x i)
(hderiv : ∀ (i : Fin d), ∀ z ∈ cubeSet Q, ‖fderiv ℝ (fun (x : Vec d) => ξ x i) z‖ ≤ B)
(hGcirc1 :
∀ (i : Fin d) (N : ℕ),
(cubeBesovCircPartialNorm Q 1 2 1 N fun (x : Vec d) => G x i) ≤ Acirc1 * √(cubeAverage Q energy))
(hGcircS :
∀ (i : Fin d) (N : ℕ),
(cubeBesovCircPartialNorm Q (1 - s) 2 1 N fun (x : Vec d) => G x i) ≤ AcircS * √(cubeAverage Q energy))
:
|cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ coarseCaccioppoliFluxEnergyExactRhs Q a s u ξ energy Acirc1 AcircS B (↑(Fintype.card (Fin d)) * C)
Compact exact-RHS local Caccioppoli estimate using full-dual vector Poincare plus the finite local-multiscale estimate.
theorem
HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_fluxEnergy_of_descendantCutoff
{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 : ℝ}
(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)
(hAcirc1 : 0 ≤ Acirc1)
(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)
(hfull : ∀ (N : ℕ), CubeDescendantDualFullVectorPoincareEstimate R C (cubeFluctuation R u) G N)
(hlocal : ∀ (N : ℕ), CubeLocalMultiscalePoincareVectorEstimate R (3 / 2 * C * 3 ^ (↑d + 1)) (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))
:
|cubeAverage R fun (x : Vec d) => vecDot (flux x) (u x • scalarCutoffGradientField η.toFun x)| ≤ coarseCaccioppoliFluxEnergyExactRhs R a s u (scalarCutoffGradientField η.toFun) energy Acirc1 AcircS
(quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2) (↑(Fintype.card (Fin d)) * C)
Exact local Caccioppoli estimate on a descendant cube using a cutoff constructed on the parent cube, with the corrected full-dual/local-multiscale Poincare inputs.
theorem
HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_split_of_fluxEnergyControl
{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 BgConst BgCent : ℝ}
(hB : 0 ≤ B)
(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))
(hBgConst : 0 ≤ BgConst)
(hBgCent : 0 ≤ BgCent)
(hC : 0 ≤ C)
(hAcirc1 : 0 ≤ Acirc1)
(hAcircS : 0 ≤ AcircS)
(henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x)
(henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume)
(hfluxCtrl : CubeAverageFluxEnergyControl Q a flux energy)
(hsum1 :
Summable fun (n : ℕ) => geometricWeight 1 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hsumS :
Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hfull : ∀ (N : ℕ), CubeDescendantDualFullVectorPoincareEstimate Q C (cubeFluctuation Q u) G N)
(hξ : ∀ (i : Fin d), ContDiff ℝ ↑⊤ fun (x : Vec d) => ξ x i)
(hderiv : ∀ (i : Fin d), ∀ z ∈ cubeSet Q, ‖fderiv ℝ (fun (x : Vec d) => ξ x i) z‖ ≤ B)
(hGcirc1 :
∀ (i : Fin d) (N : ℕ),
(cubeBesovCircPartialNorm Q 1 2 1 N fun (x : Vec d) => G x i) ≤ Acirc1 * √(cubeAverage Q energy))
(hGcircS :
∀ (i : Fin d) (N : ℕ),
(cubeBesovCircPartialNorm Q (1 - s) 2 1 N fun (x : Vec d) => G x i) ≤ AcircS * √(cubeAverage Q energy))
(hBgConst_bound : cubeLpNorm Q 2 u * (B + cubeBesovScaleWeight 1 Q * cubeLpNorm Q ⊤ ξ) ≤ BgConst)
(hBgCent_bound :
2 * (cubeScaleFactor Q * B * (√(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * (3 / 2 * (↑(Fintype.card (Fin d)) * C) * 3 ^ (↑d + 1) * (Acirc1 * √(cubeAverage Q energy)))) + cubeLpNorm Q ⊤ ξ * (cubeBesovScaleWeight (-s) Q * (3 / 2 * (↑(Fintype.card (Fin d)) * C) * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * (AcircS * √(cubeAverage Q energy))))) ≤ BgCent)
:
have E := √(cubeAverage Q energy);
have Aavg := √(coarseBBlockNorm Q a);
have Aflux1 := (geometricDiscount 1 1)⁻¹ * (LambdaSq Q 1 (MultiscaleExponent.finite 1) a).rpow (1 / 2);
have AfluxS := (geometricDiscount s 1)⁻¹ * (LambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (1 / 2);
|cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ ↑d * (3 ^ (↑d + 1) * (cubeBesovScaleWeight (-1) Q * (Aflux1 * E)) * BgConst) + (↑d * (Aavg * E * (cubeLpNorm Q ⊤ ξ * (3 / 2 * (↑(Fintype.card (Fin d)) * C) * 3 ^ (↑d + 1) * (Acirc1 * E)))) + ↑d * (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * (AfluxS * E)) * (cubeBesovScaleWeight s Q * BgCent)))
Local Caccioppoli estimate using full-dual Poincare and infinite-depth full-circ bounds, with no finite local-multiscale Poincare input.
theorem
HCPolySupport.abs_cubeAverage_vecDot_scalar_smul_le_fluxEnergyExactRhs_of_vectorFullDualFullCirc
{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 : ℝ}
(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)
(hB : 0 ≤ B)
(hAcirc1 : 0 ≤ Acirc1)
(hAcircS : 0 ≤ AcircS)
(hBgConst : 0 ≤ coarseCaccioppoliConstantCutoffSize Q u ξ B)
(hBgCent :
0 ≤ coarseCaccioppoliCenteredCutoffSize Q s ξ Acirc1 AcircS (√(cubeAverage Q energy)) B (↑(Fintype.card (Fin d)) * C))
(hC : 0 ≤ C)
(hfull : ∀ (N : ℕ), CubeDescendantDualFullVectorPoincareEstimate Q C (cubeFluctuation Q u) G N)
(hξ : ∀ (i : Fin d), ContDiff ℝ ↑⊤ fun (x : Vec d) => ξ x i)
(hderiv : ∀ (i : Fin d), ∀ z ∈ cubeSet Q, ‖fderiv ℝ (fun (x : Vec d) => ξ x i) z‖ ≤ B)
(hGcirc1 :
∀ (i : Fin d) (N : ℕ),
(cubeBesovCircPartialNorm Q 1 2 1 N fun (x : Vec d) => G x i) ≤ Acirc1 * √(cubeAverage Q energy))
(hGcircS :
∀ (i : Fin d) (N : ℕ),
(cubeBesovCircPartialNorm Q (1 - s) 2 1 N fun (x : Vec d) => G x i) ≤ AcircS * √(cubeAverage Q energy))
:
|cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ coarseCaccioppoliFluxEnergyExactRhs Q a s u ξ energy Acirc1 AcircS B (↑(Fintype.card (Fin d)) * C)
Compact exact-RHS local Caccioppoli estimate using full-dual Poincare and the infinite-depth full-circ bounds.
theorem
HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_fluxEnergyExactRhs_of_descendant
{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 : ℝ}
(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)
(hAcirc1 : 0 ≤ Acirc1)
(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)
(hfull : ∀ (N : ℕ), CubeDescendantDualFullVectorPoincareEstimate 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))
:
|cubeAverage R fun (x : Vec d) => vecDot (flux x) (u x • scalarCutoffGradientField η.toFun x)| ≤ coarseCaccioppoliFluxEnergyExactRhs R a s u (scalarCutoffGradientField η.toFun) energy Acirc1 AcircS
(quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2) (↑(Fintype.card (Fin d)) * C)
Exact local Caccioppoli estimate on a descendant cube using a parent quantitative cutoff and the full-dual/full-circ Poincare route.
theorem
HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_fluxEnergyExactRhs_of_cube_subset
{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 : ℝ}
(hsub : cubeSet R ⊆ scaledClosedCubeSet Q ρ)
(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)
(hAcirc1 : 0 ≤ Acirc1)
(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)
(hfull : ∀ (N : ℕ), CubeDescendantDualFullVectorPoincareEstimate 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))
:
|cubeAverage R fun (x : Vec d) => vecDot (flux x) (u x • scalarCutoffGradientField η.toFun x)| ≤ coarseCaccioppoliFluxEnergyExactRhs R a s u (scalarCutoffGradientField η.toFun)
((scaledClosedCubeSet Q ρ).indicator energy) Acirc1 AcircS
(quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2) (↑(Fintype.card (Fin d)) * C)
Support-localized exact-RHS estimate on the contained-descendant branch, using the full-dual/full-circ route.
theorem
HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_fluxEnergyExactRhs_of_fullDualBuffer
{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 : ℝ}
(hgap : cubeScaleFactor R ≤ (ρ - ρ₂) * cubeRadius Q)
(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)
(hAcirc1 : 0 ≤ Acirc1)
(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)
(hfull : ∀ (N : ℕ), CubeDescendantDualFullVectorPoincareEstimate 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))
:
|cubeAverage R fun (x : Vec d) => vecDot (flux x) (u x • scalarCutoffGradientField η.toFun x)| ≤ coarseCaccioppoliFluxEnergyExactRhs R a s u (scalarCutoffGradientField η.toFun)
((scaledClosedCubeSet Q ρ).indicator energy) Acirc1 AcircS
(quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2) (↑(Fintype.card (Fin d)) * C)
Buffered support-localized local exact-RHS estimate using the full-dual/full-circ route.
theorem
HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_fluxEnergyExactRhs
{d : ℕ}
(Q R : TriadicCube d)
(center : Vec d)
(a : CoeffField d)
(s : ℝ)
{rhoInner rhoOuter : ℝ}
(flux : Vec d → Vec d)
(u : Vec d → ℝ)
(G : Vec d → Vec d)
(energy : Vec d → ℝ)
{Acirc1 AcircS C : ℝ}
(hinner : 0 < rhoInner)
(hinnerOuter : rhoInner < rhoOuter)
(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 / ((rhoOuter - rhoInner) * (cubeRadius Q / 3)) ^ 2)
(hAcirc1 : 0 ≤ Acirc1)
(hAcircS : 0 ≤ AcircS)
(hBgConst :
0 ≤ coarseCaccioppoliConstantCutoffSize R u
(scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter))
(quantitativeCubeCutoffHessianConst d / ((rhoOuter - rhoInner) * (cubeRadius Q / 3)) ^ 2))
(hBgCent :
0 ≤ coarseCaccioppoliCenteredCutoffSize R s
(scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter)) Acirc1 AcircS
(√(cubeAverage R energy))
(quantitativeCubeCutoffHessianConst d / ((rhoOuter - rhoInner) * (cubeRadius Q / 3)) ^ 2)
(↑(Fintype.card (Fin d)) * C))
(hC : 0 ≤ C)
(hfull : ∀ (N : ℕ), CubeDescendantDualFullVectorPoincareEstimate 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))
:
|cubeAverage R fun (x : Vec d) =>
vecDot (flux x)
(u x • scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter) x)| ≤ coarseCaccioppoliFluxEnergyExactRhs R a s u
(scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter)) energy Acirc1 AcircS
(quantitativeCubeCutoffHessianConst d / ((rhoOuter - rhoInner) * (cubeRadius Q / 3)) ^ 2)
(↑(Fintype.card (Fin d)) * C)
Exact local Caccioppoli estimate on a cube using the arbitrary-center local canonical cutoff and the full-dual/full-circ route.
theorem
HCPolySupport.cubeAveragePairingAbs_le_fluxEnergyIndicator_of_fullDualPoincare
{d : ℕ}
{Q R : TriadicCube d}
(center : Vec d)
(a : CoeffField d)
(s : ℝ)
{rhoInner rhoOuter rho : ℝ}
(flux : Vec d → Vec d)
(u : Vec d → ℝ)
(G : Vec d → Vec d)
(energy : Vec d → ℝ)
{Acirc1 AcircS C : ℝ}
(hinner : 0 < rhoInner)
(hinnerOuter : rhoInner < rhoOuter)
(hsub : cubeSet R ⊆ coarseCaccioppoliLocalClosedCube Q center rho)
(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 / ((rhoOuter - rhoInner) * (cubeRadius Q / 3)) ^ 2)
(hAcirc1 : 0 ≤ Acirc1)
(hAcircS : 0 ≤ AcircS)
(hBgConst :
0 ≤ coarseCaccioppoliConstantCutoffSize R u
(scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter))
(quantitativeCubeCutoffHessianConst d / ((rhoOuter - rhoInner) * (cubeRadius Q / 3)) ^ 2))
(hBgCent :
0 ≤ coarseCaccioppoliCenteredCutoffSize R s
(scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter)) Acirc1 AcircS
(√(cubeAverage R energy))
(quantitativeCubeCutoffHessianConst d / ((rhoOuter - rhoInner) * (cubeRadius Q / 3)) ^ 2)
(↑(Fintype.card (Fin d)) * C))
(hC : 0 ≤ C)
(hfull : ∀ (N : ℕ), CubeDescendantDualFullVectorPoincareEstimate 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))
:
|cubeAverage R fun (x : Vec d) =>
vecDot (flux x)
(u x • scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter) x)| ≤ coarseCaccioppoliFluxEnergyExactRhs R a s u
(scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter))
((coarseCaccioppoliLocalClosedCube Q center rho).indicator energy) Acirc1 AcircS
(quantitativeCubeCutoffHessianConst d / ((rhoOuter - rhoInner) * (cubeRadius Q / 3)) ^ 2)
(↑(Fintype.card (Fin d)) * C)
Local exact-RHS estimate for the arbitrary-center canonical cutoff, with the RHS energy localized to a larger local cube, on the contained branch of the full-dual/full-circ route.
theorem
HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_fluxEnergyExactRhs_of_localBuffer
{d : ℕ}
{Q R : TriadicCube d}
{j : ℕ}
(_hR : R ∈ descendantsAtDepth Q j)
(center : Vec d)
(a : CoeffField d)
(s : ℝ)
{rhoInner rhoOuter rho : ℝ}
(flux : Vec d → Vec d)
(u : Vec d → ℝ)
(G : Vec d → Vec d)
(energy : Vec d → ℝ)
{Acirc1 AcircS C : ℝ}
(hinner : 0 < rhoInner)
(hinnerOuter : rhoInner < rhoOuter)
(hgap : cubeScaleFactor R ≤ (rho - rhoOuter) * (cubeRadius Q / 3))
(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 / ((rhoOuter - rhoInner) * (cubeRadius Q / 3)) ^ 2)
(hAcirc1 : 0 ≤ Acirc1)
(hAcircS : 0 ≤ AcircS)
(hBgConst :
0 ≤ coarseCaccioppoliConstantCutoffSize R u
(scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter))
(quantitativeCubeCutoffHessianConst d / ((rhoOuter - rhoInner) * (cubeRadius Q / 3)) ^ 2))
(hBgCent :
0 ≤ coarseCaccioppoliCenteredCutoffSize R s
(scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter)) Acirc1 AcircS
(√(cubeAverage R energy))
(quantitativeCubeCutoffHessianConst d / ((rhoOuter - rhoInner) * (cubeRadius Q / 3)) ^ 2)
(↑(Fintype.card (Fin d)) * C))
(hC : 0 ≤ C)
(hfull : ∀ (N : ℕ), CubeDescendantDualFullVectorPoincareEstimate 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))
:
|cubeAverage R fun (x : Vec d) =>
vecDot (flux x)
(u x • scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter) x)| ≤ coarseCaccioppoliFluxEnergyExactRhs R a s u
(scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter))
((coarseCaccioppoliLocalClosedCube Q center rho).indicator energy) Acirc1 AcircS
(quantitativeCubeCutoffHessianConst d / ((rhoOuter - rhoInner) * (cubeRadius Q / 3)) ^ 2)
(↑(Fintype.card (Fin d)) * C)
Buffered local exact-RHS estimate for the arbitrary-center canonical cutoff using the full-dual/full-circ route.