Coarse-graining support: Support.Deterministic.CoarseCaccioppoli.EnergyBridge.DescendantSummation #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Descendant summation for the small-cube Caccioppoli route #
The LaTeX proof estimates the cutoff pairing on small cubes and then sums over
those cubes. This file isolates the measure-theoretic bookkeeping: a
cube-average over Q is the descendants-average of the cube-averages over the
depth-j descendants, hence its absolute value is controlled by the
descendants-average of the local absolute values.
theorem
HCPolySupport.abs_cubeAverage_vecDot_scalar_smul_le_raw_of_parentQuantitativeCutoff_on_descendants
{d : ℕ}
{Q : TriadicCube d}
(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 Alpha Bcross : ℝ}
(hs0 : 0 < s)
(hs1 : s < 1)
(hpair_int :
MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (flux x) (u x • scalarCutoffGradientField η.toFun x))
(cubeSet Q) MeasureTheory.volume)
(huQ : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x)
(henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume)
(hfluxMem : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp flux 2 (normalizedCubeMeasure R))
(hu : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp u 2 (normalizedCubeMeasure R))
(hG :
∀ R ∈ descendantsAtDepth Q j,
∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure R))
(hfluxEnergy : ∀ R ∈ descendantsAtDepth Q j, CoarseCaccioppoliFluxEnergyControls R a s flux energy)
(hB : 0 ≤ quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2)
(hAcircS : 0 ≤ AcircS)
(hBgConst :
∀ R ∈ descendantsAtDepth Q j,
0 ≤ coarseCaccioppoliConstantCutoffSize R u (scalarCutoffGradientField η.toFun)
(quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2))
(hBgCent :
∀ R ∈ descendantsAtDepth Q j,
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 :
∀ R ∈ descendantsAtDepth Q j,
∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate R C (cubeFluctuation R u) G N)
(hGcirc1 :
∀ R ∈ descendantsAtDepth Q j,
∀ (i : Fin d) (N : ℕ),
(cubeBesovCircPartialNorm R 1 2 1 N fun (x : Vec d) => G x i) ≤ Acirc1 * √(cubeAverage R energy))
(hGcircS :
∀ R ∈ descendantsAtDepth Q j,
∀ (i : Fin d) (N : ℕ),
(cubeBesovCircPartialNorm R (1 - s) 2 1 N fun (x : Vec d) => G x i) ≤ AcircS * √(cubeAverage R energy))
(hK_nonneg : 0 ≤ K)
(hKparent : K * cubeLpNorm Q 2 u ≤ Bcross)
(hconst :
∀ R ∈ descendantsAtDepth Q j,
coarseCaccioppoliFluxEnergyExactConstantCoeff R a * (quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2 + cubeBesovScaleWeight 1 R * cubeLpNorm R ⊤ (scalarCutoffGradientField η.toFun)) ≤ K)
(hcent :
∀ R ∈ descendantsAtDepth Q j,
coarseCaccioppoliFluxEnergyExactCenteredCoeff R a s (scalarCutoffGradientField η.toFun) Acirc1 AcircS
(quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2) (↑(Fintype.card (Fin d)) * C) ≤ Alpha)
:
|cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • scalarCutoffGradientField η.toFun x)| ≤ Alpha * cubeAverage Q energy + Bcross * √(cubeAverage Q energy)
Small-cube Caccioppoli estimate in the exact-RHS proof shape.
This theorem is the direct descendant route: estimate the cutoff pairing on
each depth-j cube using the parent quantitative cutoff, average the local
exact RHS values, and collapse the result to the parent raw RHS by finite
Cauchy.
theorem
HCPolySupport.abs_cubeAverage_fluxCutoff_le_raw_of_parentCutoff_variableCirc
{d : ℕ}
{Q : TriadicCube d}
(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 : TriadicCube d → ℝ)
{C K Alpha Bcross : ℝ}
(hs0 : 0 < s)
(hs1 : s < 1)
(hpair_int :
MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (flux x) (u x • scalarCutoffGradientField η.toFun x))
(cubeSet Q) MeasureTheory.volume)
(huQ : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x)
(henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume)
(hfluxMem : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp flux 2 (normalizedCubeMeasure R))
(hu : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp u 2 (normalizedCubeMeasure R))
(hG :
∀ R ∈ descendantsAtDepth Q j,
∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure R))
(hfluxEnergy : ∀ R ∈ descendantsAtDepth Q j, CoarseCaccioppoliFluxEnergyControls R a s flux energy)
(hB : 0 ≤ quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2)
(hAcircS : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ AcircS R)
(hBgConst :
∀ R ∈ descendantsAtDepth Q j,
0 ≤ coarseCaccioppoliConstantCutoffSize R u (scalarCutoffGradientField η.toFun)
(quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2))
(hBgCent :
∀ R ∈ descendantsAtDepth Q j,
0 ≤ coarseCaccioppoliCenteredCutoffSize R s (scalarCutoffGradientField η.toFun) (Acirc1 R) (AcircS R)
(√(cubeAverage R energy)) (quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2)
(↑(Fintype.card (Fin d)) * C))
(hC : 0 ≤ C)
(hproj :
∀ R ∈ descendantsAtDepth Q j,
∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate R C (cubeFluctuation R u) G N)
(hGcirc1 :
∀ R ∈ descendantsAtDepth Q j,
∀ (i : Fin d) (N : ℕ),
(cubeBesovCircPartialNorm R 1 2 1 N fun (x : Vec d) => G x i) ≤ Acirc1 R * √(cubeAverage R energy))
(hGcircS :
∀ R ∈ descendantsAtDepth Q j,
∀ (i : Fin d) (N : ℕ),
(cubeBesovCircPartialNorm R (1 - s) 2 1 N fun (x : Vec d) => G x i) ≤ AcircS R * √(cubeAverage R energy))
(hK_nonneg : 0 ≤ K)
(hKparent : K * cubeLpNorm Q 2 u ≤ Bcross)
(hconst :
∀ R ∈ descendantsAtDepth Q j,
coarseCaccioppoliFluxEnergyExactConstantCoeff R a * (quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2 + cubeBesovScaleWeight 1 R * cubeLpNorm R ⊤ (scalarCutoffGradientField η.toFun)) ≤ K)
(hcent :
∀ R ∈ descendantsAtDepth Q j,
coarseCaccioppoliFluxEnergyExactCenteredCoeff R a s (scalarCutoffGradientField η.toFun) (Acirc1 R) (AcircS R)
(quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2) (↑(Fintype.card (Fin d)) * C) ≤ Alpha)
:
|cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • scalarCutoffGradientField η.toFun x)| ≤ Alpha * cubeAverage Q energy + Bcross * √(cubeAverage Q energy)
Variable-Acirc version of
abs_cubeAverage_vecDot_scalar_smul_le_raw_of_parentQuantitativeCutoff_on_descendants.
The local descendant pairing and the averaged exact RHS both use
Acirc1 R and AcircS R.
theorem
HCPolySupport.abs_cubeAverage_vecDot_scalar_smul_le_localized_raw_of_local_exactRhs_bounds_variableAcirc
{d : ℕ}
{Q : TriadicCube d}
(j : ℕ)
(ρ : ℝ)
(a : CoeffField d)
(s : ℝ)
(flux : Vec d → Vec d)
(u : Vec d → ℝ)
(ξ : Vec d → Vec d)
(energy : Vec d → ℝ)
(Acirc1 AcircS : TriadicCube d → ℝ)
{B C K Alpha Bcross : ℝ}
(hpair_int :
MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (flux x) (u x • ξ x)) (cubeSet Q) MeasureTheory.volume)
(huQ : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x)
(henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume)
(hK_nonneg : 0 ≤ K)
(hKparent : K * cubeLpNorm Q 2 u ≤ Bcross)
(hconst :
∀ R ∈ descendantsAtDepth Q j,
coarseCaccioppoliFluxEnergyExactConstantCoeff R a * (B + cubeBesovScaleWeight 1 R * cubeLpNorm R ⊤ ξ) ≤ K)
(hcent :
∀ R ∈ descendantsAtDepth Q j, coarseCaccioppoliFluxEnergyExactCenteredCoeff R a s ξ (Acirc1 R) (AcircS R) B C ≤ Alpha)
(hlocal :
∀ R ∈ descendantsAtDepth Q j,
|cubeAverage R fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ coarseCaccioppoliFluxEnergyExactRhs R a s u ξ ((scaledClosedCubeSet Q ρ).indicator energy) (Acirc1 R) (AcircS R) B
C)
:
|cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ Alpha * coarseCaccioppoliLocalizedEnergyProfile Q ρ energy + Bcross * √(coarseCaccioppoliLocalizedEnergyProfile Q ρ energy)
Localized-energy descendant summation for a cutoff pairing, assuming the local descendant bounds are already stated with the outer-radius localized energy density.
This is the purely summation-level replacement for the old final rewrite by a
full-cube/localized energy equality: the parent exact-RHS collapse is performed
directly on (scaledClosedCubeSet Q ρ).indicator energy.
theorem
HCPolySupport.abs_cubeAverage_vecDot_scalar_smul_le_localPatch_raw_of_local_exactRhs_bounds_variableAcirc
{d : ℕ}
{Q : TriadicCube d}
(center : Vec d)
(j : ℕ)
(rho : ℝ)
(a : CoeffField d)
(s : ℝ)
(flux : Vec d → Vec d)
(u : Vec d → ℝ)
(ξ : Vec d → Vec d)
(energy : Vec d → ℝ)
(Acirc1 AcircS : TriadicCube d → ℝ)
{B C K Alpha Bcross : ℝ}
(hpair_int :
MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (flux x) (u x • ξ x)) (cubeSet Q) MeasureTheory.volume)
(huQ : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x)
(henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume)
(hK_nonneg : 0 ≤ K)
(hKparent : K * cubeLpNorm Q 2 u ≤ Bcross)
(hconst :
∀ R ∈ descendantsAtDepth Q j,
coarseCaccioppoliFluxEnergyExactConstantCoeff R a * (B + cubeBesovScaleWeight 1 R * cubeLpNorm R ⊤ ξ) ≤ K)
(hcent :
∀ R ∈ descendantsAtDepth Q j, coarseCaccioppoliFluxEnergyExactCenteredCoeff R a s ξ (Acirc1 R) (AcircS R) B C ≤ Alpha)
(hlocal :
∀ R ∈ descendantsAtDepth Q j,
|cubeAverage R fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ coarseCaccioppoliFluxEnergyExactRhs R a s u ξ ((coarseCaccioppoliLocalClosedCube Q center rho).indicator energy)
(Acirc1 R) (AcircS R) B C)
:
|cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ Alpha * coarseCaccioppoliLocalEnergyProfile Q center rho energy + Bcross * √(coarseCaccioppoliLocalEnergyProfile Q center rho energy)
Arbitrary-center local-patch analogue of
abs_cubeAverage_vecDot_scalar_smul_le_localized_raw_of_local_exactRhs_bounds_variableAcirc.
theorem
HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_raw
{d : ℕ}
{Q : TriadicCube d}
(j : ℕ)
(a : CoeffField d)
(s : ℝ)
{ρ₁ ρ₂ : ℝ}
(flux : Vec d → Vec d)
(u energy : Vec d → ℝ)
(η : QuantitativeCubeCutoff Q ρ₁ ρ₂)
(Acirc1 AcircS : TriadicCube d → ℝ)
{B C K Alpha Bcross : ℝ}
(hpair_int :
MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (flux x) (u x • scalarCutoffGradientField η.toFun x))
(cubeSet Q) MeasureTheory.volume)
(huQ : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x)
(henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume)
(hK_nonneg : 0 ≤ K)
(hKparent : K * cubeLpNorm Q 2 u ≤ Bcross)
(hconst :
∀ R ∈ descendantsAtDepth Q j,
coarseCaccioppoliFluxEnergyExactConstantCoeff R a * (B + cubeBesovScaleWeight 1 R * cubeLpNorm R ⊤ (scalarCutoffGradientField η.toFun)) ≤ K)
(hcent :
∀ R ∈ descendantsAtDepth Q j,
coarseCaccioppoliFluxEnergyExactCenteredCoeff R a s (scalarCutoffGradientField η.toFun) (Acirc1 R) (AcircS R) B C ≤ Alpha)
(hlocal :
∀ R ∈ descendantsAtDepth Q j,
|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 R) (AcircS R) B C)
:
|cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • scalarCutoffGradientField η.toFun x)| ≤ Alpha * coarseCaccioppoliLocalizedEnergyProfile Q ρ₂ energy + Bcross * √(coarseCaccioppoliLocalizedEnergyProfile Q ρ₂ energy)
Parent-cutoff specialization of
abs_cubeAverage_vecDot_scalar_smul_le_localized_raw_of_local_exactRhs_bounds_variableAcirc.
The only analytic input not supplied here is the genuinely local, support-aware exact-RHS estimate with the outer localized energy density.
theorem
HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_raw_of_support_buffer_of_buffer
{d : ℕ}
{Q : TriadicCube d}
(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 : TriadicCube d → ℝ)
{C K Alpha Bcross : ℝ}
(hs0 : 0 < s)
(hs1 : s < 1)
(hbuffer : ∀ R ∈ descendantsAtDepth Q j, cubeScaleFactor R ≤ (ρ - ρ₂) * cubeRadius Q)
(hpair_int :
MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (flux x) (u x • scalarCutoffGradientField η.toFun x))
(cubeSet Q) MeasureTheory.volume)
(huQ : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x)
(henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume)
(hfluxMem : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp flux 2 (normalizedCubeMeasure R))
(hu : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp u 2 (normalizedCubeMeasure R))
(hG :
∀ R ∈ descendantsAtDepth Q j,
∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure R))
(hfluxEnergy : ∀ R ∈ descendantsAtDepth Q j, CoarseCaccioppoliFluxEnergyControls R a s flux energy)
(hB : 0 ≤ quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2)
(hAcirc1 : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ Acirc1 R)
(hAcircS : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ AcircS R)
(hBgConst :
∀ R ∈ descendantsAtDepth Q j,
0 ≤ coarseCaccioppoliConstantCutoffSize R u (scalarCutoffGradientField η.toFun)
(quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2))
(hBgCent :
∀ R ∈ descendantsAtDepth Q j,
0 ≤ coarseCaccioppoliCenteredCutoffSize R s (scalarCutoffGradientField η.toFun) (Acirc1 R) (AcircS R)
(√(cubeAverage R energy)) (quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2)
(↑(Fintype.card (Fin d)) * C))
(hC : 0 ≤ C)
(hproj :
∀ R ∈ descendantsAtDepth Q j,
∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate R C (cubeFluctuation R u) G N)
(hGcirc1 :
∀ R ∈ descendantsAtDepth Q j,
∀ (i : Fin d) (N : ℕ),
(cubeBesovCircPartialNorm R 1 2 1 N fun (x : Vec d) => G x i) ≤ Acirc1 R * √(cubeAverage R energy))
(hGcircS :
∀ R ∈ descendantsAtDepth Q j,
∀ (i : Fin d) (N : ℕ),
(cubeBesovCircPartialNorm R (1 - s) 2 1 N fun (x : Vec d) => G x i) ≤ AcircS R * √(cubeAverage R energy))
(hK_nonneg : 0 ≤ K)
(hKparent : K * cubeLpNorm Q 2 u ≤ Bcross)
(hconst :
∀ R ∈ descendantsAtDepth Q j,
coarseCaccioppoliFluxEnergyExactConstantCoeff R a * (quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2 + cubeBesovScaleWeight 1 R * cubeLpNorm R ⊤ (scalarCutoffGradientField η.toFun)) ≤ K)
(hcent :
∀ R ∈ descendantsAtDepth Q j,
coarseCaccioppoliFluxEnergyExactCenteredCoeff R a s (scalarCutoffGradientField η.toFun) (Acirc1 R) (AcircS R)
(quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2) (↑(Fintype.card (Fin d)) * C) ≤ Alpha)
:
|cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • scalarCutoffGradientField η.toFun x)| ≤ Alpha * coarseCaccioppoliLocalizedEnergyProfile Q ρ energy + Bcross * √(coarseCaccioppoliLocalizedEnergyProfile Q ρ energy)
Buffered localized-energy descendant summation for a parent cutoff.
The cutoff is supported in scaledClosedCubeSet Q ρ₂, while the RHS energy is
localized on the larger radius ρ. The buffer hypothesis says every
depth-j descendant is small enough that a cube touching the cutoff support is
contained in the larger localization cube; descendants missing the support have
zero local pairing.
theorem
HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_local_raw_of_support_buffer
{d : ℕ}
{Q : TriadicCube d}
(center : Vec d)
(j : ℕ)
(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 : TriadicCube d → ℝ)
{C K Alpha Bcross : ℝ}
(hinner : 0 < rhoInner)
(hinnerOuter : rhoInner < rhoOuter)
(hs0 : 0 < s)
(hs1 : s < 1)
(hbuffer : ∀ R ∈ descendantsAtDepth Q j, cubeScaleFactor R ≤ (rho - rhoOuter) * (cubeRadius Q / 3))
(hpair_int :
MeasureTheory.IntegrableOn
(fun (x : Vec d) =>
vecDot (flux x)
(u x • scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter) x))
(cubeSet Q) MeasureTheory.volume)
(huQ : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x)
(henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume)
(hfluxMem : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp flux 2 (normalizedCubeMeasure R))
(hu : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp u 2 (normalizedCubeMeasure R))
(hG :
∀ R ∈ descendantsAtDepth Q j,
∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure R))
(hfluxEnergy : ∀ R ∈ descendantsAtDepth Q j, CoarseCaccioppoliFluxEnergyControls R a s flux energy)
(hB : 0 ≤ quantitativeCubeCutoffHessianConst d / ((rhoOuter - rhoInner) * (cubeRadius Q / 3)) ^ 2)
(hAcirc1 : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ Acirc1 R)
(hAcircS : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ AcircS R)
(hBgConst :
∀ R ∈ descendantsAtDepth Q j,
0 ≤ coarseCaccioppoliConstantCutoffSize R u
(scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter))
(quantitativeCubeCutoffHessianConst d / ((rhoOuter - rhoInner) * (cubeRadius Q / 3)) ^ 2))
(hBgCent :
∀ R ∈ descendantsAtDepth Q j,
0 ≤ coarseCaccioppoliCenteredCutoffSize R s
(scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter)) (Acirc1 R)
(AcircS R) (√(cubeAverage R energy))
(quantitativeCubeCutoffHessianConst d / ((rhoOuter - rhoInner) * (cubeRadius Q / 3)) ^ 2)
(↑(Fintype.card (Fin d)) * C))
(hC : 0 ≤ C)
(hproj :
∀ R ∈ descendantsAtDepth Q j,
∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate R C (cubeFluctuation R u) G N)
(hGcirc1 :
∀ R ∈ descendantsAtDepth Q j,
∀ (i : Fin d) (N : ℕ),
(cubeBesovCircPartialNorm R 1 2 1 N fun (x : Vec d) => G x i) ≤ Acirc1 R * √(cubeAverage R energy))
(hGcircS :
∀ R ∈ descendantsAtDepth Q j,
∀ (i : Fin d) (N : ℕ),
(cubeBesovCircPartialNorm R (1 - s) 2 1 N fun (x : Vec d) => G x i) ≤ AcircS R * √(cubeAverage R energy))
(hK_nonneg : 0 ≤ K)
(hKparent : K * cubeLpNorm Q 2 u ≤ Bcross)
(hconst :
∀ R ∈ descendantsAtDepth Q j,
coarseCaccioppoliFluxEnergyExactConstantCoeff R a * (quantitativeCubeCutoffHessianConst d / ((rhoOuter - rhoInner) * (cubeRadius Q / 3)) ^ 2 + cubeBesovScaleWeight 1 R * cubeLpNorm R ⊤
(scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter))) ≤ K)
(hcent :
∀ R ∈ descendantsAtDepth Q j,
coarseCaccioppoliFluxEnergyExactCenteredCoeff R a s
(scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter)) (Acirc1 R)
(AcircS R) (quantitativeCubeCutoffHessianConst d / ((rhoOuter - rhoInner) * (cubeRadius Q / 3)) ^ 2)
(↑(Fintype.card (Fin d)) * C) ≤ Alpha)
:
|cubeAverage Q fun (x : Vec d) =>
vecDot (flux x)
(u x • scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter) x)| ≤ Alpha * coarseCaccioppoliLocalEnergyProfile Q center rho energy + Bcross * √(coarseCaccioppoliLocalEnergyProfile Q center rho energy)
Buffered arbitrary-center local-patch descendant summation for the translated canonical cutoff. This is the summation-level form of the boundary Caccioppoli radius step from the notes.