Coarse-graining support: Support.Deterministic.CoarseCaccioppoli.EnergyBridge.LocalEstimate.Cutoff

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

Local energy estimate: cutoff-localized exact RHS bridge

theorem HCPolySupport.abs_cubeAverage_fluxCutoff_le_exactRhs_of_parentCutoff {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) (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)) : |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. This is the small-cube local form of the Chapter 3 proof: the cube being averaged is R, while the cutoff transition still comes from the annulus between the two radii of Q.

theorem HCPolySupport.abs_cubeAverage_vecDot_scalar_smul_le_fluxEnergyExactRhs_of_localCanonicalCutoff_on_cube {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) (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) (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)) : |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. This is the single-cube bridge needed by the boundary radius profile in the notes, where the cutoff lives on center + rho cu_{m-1} rather than on a cube centered at the parent cube center.

theorem HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_fluxEnergyExactRhs_indicator {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) (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) (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)) : |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 arbitrary-center local cube, on the branch where the averaged cube is contained in that larger local cube.

theorem HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_fluxEnergyExactRhs_of_forall_notMem {d : ℕ} {Q R : TriadicCube d} (center : Vec d) (a : CoeffField d) {s rhoInner rhoOuter rho : ℝ} (flux : Vec d → Vec d) (u energy : Vec d → ℝ) {Acirc1 AcircS B C : ℝ} (hinner : 0 < rhoInner) (hinnerOuter : rhoInner < rhoOuter) (hout : ∀ x ∈ cubeSet R, x ∉ coarseCaccioppoliLocalClosedCube Q center rhoOuter) (hs : 0 < s) (hAcirc1 : 0 ≤ Acirc1) (hAcircS : 0 ≤ AcircS) (hB : 0 ≤ B) (hC : 0 ≤ C) : |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 B C

Local exact-RHS estimate for descendant cubes outside the support of the arbitrary-center canonical cutoff. The pairing vanishes pointwise on the averaged cube.

theorem HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_fluxEnergyExactRhs_of_support_buffer {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) (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)) : |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. A descendant either misses the local cutoff support or, if it touches the support, the buffer hypothesis forces it into the larger local energy cube.

theorem HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_fluxEnergyExactRhs_of_cubeSubset {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) (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)) : |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)

Local exact-RHS estimate with an outer localized energy density, for descendant cubes contained in the localization region.

This is the support-localized version of abs_cubeAverage_vecDot_scalar_smul_le_fluxEnergyExactRhs_of_parentQuantitativeCutoff_on_descendant on the easy branch: when cubeSet R is contained in the outer scaled cube, the localized indicator agrees with the original energy on every descendant of R, so the flux-energy controls and the scalar bounds transfer by cube-average congruence.

theorem HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_fluxEnergyExactRhs_of_notMem {d : ℕ} {Q R : TriadicCube d} (a : CoeffField d) {s ρ₁ ρ₂ ρ : ℝ} (flux : Vec d → Vec d) (u energy : Vec d → ℝ) (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) {Acirc1 AcircS B C : ℝ} (hout : ∀ x ∈ cubeSet R, x ∉ scaledClosedCubeSet Q ρ₂) (hs : 0 < s) (hAcirc1 : 0 ≤ Acirc1) (hAcircS : 0 ≤ AcircS) (hB : 0 ≤ B) (hC : 0 ≤ C) : |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 B C

Local exact-RHS estimate with an outer localized energy density, for descendant cubes outside the support region of the parent cutoff. In this branch the pairing vanishes pointwise on the averaged cube.

theorem HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_fluxEnergyExactRhs_of_parentBuffer {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) (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)) : |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 local exact-RHS estimate. The cutoff is supported in scaledClosedCubeSet Q ρ₂, while the energy is localized on a larger radius ρ. If the descendant side length fits in the buffer ρ - ρ₂, then every descendant either misses the cutoff support, or is entirely contained in the larger localization cube.