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

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

Arbitrary-center local cutoffs for coarse Caccioppoli

The boundary Caccioppoli proof in the notes uses cutoffs on (center + rho cu_{m-1}) ∩ cu_m, with arbitrary patch center center. The older deterministic stack used only cutoffs centered at the parent cube center. This file reuses the canonical cube cutoff on the origin cube of scale Q.scale - 1, translated to the desired local center.

def HCPolySupport.coarseCaccioppoliLocalReferenceCube {d : ℕ} (Q : TriadicCube d) : TriadicCube d

Reference origin cube with the scale of cu_{m-1} when Q has scale m.

Equations

• HCPolySupport.coarseCaccioppoliLocalReferenceCube Q = HCPolySupport.originCube d (Q.scale - 1)

theorem HCPolySupport.cubeCenter_coarseCaccioppoliLocalReferenceCube {d : ℕ} (Q : TriadicCube d) : cubeCenter (coarseCaccioppoliLocalReferenceCube Q) = 0

theorem HCPolySupport.cubeRadius_coarseCaccioppoliLocalReferenceCube {d : ℕ} (Q : TriadicCube d) : cubeRadius (coarseCaccioppoliLocalReferenceCube Q) = cubeRadius Q / 3

theorem HCPolySupport.sub_center_mem_scaledClosedCubeSet_localReference_iff {d : ℕ} (Q : TriadicCube d) (center x : Vec d) (rho : ℝ) : x - center ∈ scaledClosedCubeSet (coarseCaccioppoliLocalReferenceCube Q) rho ↔ x ∈ coarseCaccioppoliLocalClosedCube Q center rho

theorem HCPolySupport.sub_center_mem_scaledOpenCubeSet_localReference_iff {d : ℕ} (Q : TriadicCube d) (center x : Vec d) (rho : ℝ) : x - center ∈ scaledOpenCubeSet (coarseCaccioppoliLocalReferenceCube Q) rho ↔ x ∈ coarseCaccioppoliLocalOpenCube Q center rho

theorem HCPolySupport.cubeSet_subset_coarseCaccioppoliLocalClosedCube_of_intersects_of_scaleFactor_le_gap {d : ℕ} {Q R : TriadicCube d} {center : Vec d} {rhoInner rhoOuter : ℝ} (hgap : cubeScaleFactor R ≤ (rhoOuter - rhoInner) * (cubeRadius Q / 3)) (hinter : ∃ y ∈ cubeSet R, y ∈ coarseCaccioppoliLocalClosedCube Q center rhoInner) : cubeSet R ⊆ coarseCaccioppoliLocalClosedCube Q center rhoOuter

If a descendant cube touches an inner local cube and is smaller than the local radial buffer, then it is contained in the outer local cube.

noncomputable def HCPolySupport.coarseCaccioppoliLocalCanonicalFun {d : ℕ} (Q : TriadicCube d) (center : Vec d) (rhoInner rhoOuter : ℝ) : Vec d → ℝ

Canonical local cutoff centered at an arbitrary patch center.

Equations

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

theorem HCPolySupport.coarseCaccioppoliLocalCanonicalFun_smooth {d : ℕ} (Q : TriadicCube d) (center : Vec d) {rhoInner rhoOuter : ℝ} (hinner : 0 < rhoInner) (hinnerOuter : rhoInner < rhoOuter) : ContDiff ℝ (↑⊤) (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter)

theorem HCPolySupport.coarseCaccioppoliLocalCanonicalFun_nonneg {d : ℕ} (Q : TriadicCube d) (center : Vec d) (rhoInner rhoOuter : ℝ) (x : Vec d) : 0 ≤ coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter x

theorem HCPolySupport.coarseCaccioppoliLocalCanonicalFun_le_one {d : ℕ} (Q : TriadicCube d) (center : Vec d) (rhoInner rhoOuter : ℝ) (x : Vec d) : coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter x ≤ 1

theorem HCPolySupport.coarseCaccioppoliLocalCanonicalFun_hasCompactSupport {d : ℕ} (Q : TriadicCube d) (center : Vec d) {rhoInner rhoOuter : ℝ} (hinner : 0 < rhoInner) (hinnerOuter : rhoInner < rhoOuter) : HasCompactSupport (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter)

theorem HCPolySupport.integrableOn_localCanonicalCutoff_mul_of_integrableOn_cubeSet {d : ℕ} (Q : TriadicCube d) (center : Vec d) {rhoInner rhoOuter : ℝ} {energy : Vec d → ℝ} (hinner : 0 < rhoInner) (hinnerOuter : rhoInner < rhoOuter) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (x : Vec d) => coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter x * energy x) (cubeSet Q) MeasureTheory.volume

Multiplication by the translated local canonical cutoff preserves parent-cube integrability.

theorem HCPolySupport.coarseCaccioppoliLocalCanonicalFun_eq_one_on_inner {d : ℕ} {Q : TriadicCube d} {center : Vec d} {rhoInner rhoOuter : ℝ} (hinner : 0 < rhoInner) (hinnerOuter : rhoInner < rhoOuter) {x : Vec d} (hx : x ∈ coarseCaccioppoliLocalClosedCube Q center rhoInner) : coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter x = 1

theorem HCPolySupport.coarseCaccioppoliLocalEnergyProfile_le_localCanonicalCutoffEnergy {d : ℕ} (Q : TriadicCube d) (center : Vec d) {rhoInner rhoOuter : ℝ} (energy : Vec d → ℝ) (hinner : 0 < rhoInner) (hinnerOuter : rhoInner < rhoOuter) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (hprofile_int : MeasureTheory.IntegrableOn ((coarseCaccioppoliLocalClosedCube Q center rhoInner).indicator energy) (cubeSet Q) MeasureTheory.volume) (hweighted_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter x * energy x) (cubeSet Q) MeasureTheory.volume) : coarseCaccioppoliLocalEnergyProfile Q center rhoInner energy ≤ cubeAverage Q fun (x : Vec d) => coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter x * energy x

The local inner energy is bounded by the translated canonical cutoff-weighted energy.

theorem HCPolySupport.coarseCaccioppoliLocalEnergyProfile_le_localCanonicalCutoffEnergy_of_integrable {d : ℕ} (Q : TriadicCube d) (center : Vec d) {rhoInner rhoOuter : ℝ} (energy : Vec d → ℝ) (hinner : 0 < rhoInner) (hinnerOuter : rhoInner < rhoOuter) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) : coarseCaccioppoliLocalEnergyProfile Q center rhoInner energy ≤ cubeAverage Q fun (x : Vec d) => coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter x * energy x

Integrability-free local lower bound using the translated canonical cutoff.

theorem HCPolySupport.coarseCaccioppoliLocalCanonicalFun_support_subset_localOpenCube {d : ℕ} {Q : TriadicCube d} {center : Vec d} {rhoInner rhoOuter : ℝ} (hinner : 0 < rhoInner) (hinnerOuter : rhoInner < rhoOuter) : Function.support (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter) ⊆ coarseCaccioppoliLocalOpenCube Q center rhoOuter

theorem HCPolySupport.coarseCaccioppoliLocalCanonicalFun_tsupport_subset_localClosedCube {d : ℕ} {Q : TriadicCube d} {center : Vec d} {rhoInner rhoOuter : ℝ} (hinner : 0 < rhoInner) (hinnerOuter : rhoInner < rhoOuter) : tsupport (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter) ⊆ coarseCaccioppoliLocalClosedCube Q center rhoOuter

theorem HCPolySupport.coarseCaccioppoliLocalCanonicalFun_tsupport_subset_openCubeSet {d : ℕ} {Q : TriadicCube d} {center : Vec d} {rhoInner rhoOuter : ℝ} (hinner : 0 < rhoInner) (hinnerOuter : rhoInner < rhoOuter) (hsub : coarseCaccioppoliLocalClosedCube Q center rhoOuter ⊆ openCubeSet Q) : tsupport (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter) ⊆ openCubeSet Q

theorem HCPolySupport.coarseCaccioppoliLocalClosedCube_subset_localOpenCube_one_of_lt_one {d : ℕ} {Q : TriadicCube d} {center : Vec d} {rho : ℝ} (hrho : rho < 1) : coarseCaccioppoliLocalClosedCube Q center rho ⊆ coarseCaccioppoliLocalOpenCube Q center 1

theorem HCPolySupport.support_scalarCutoffGradientField_coarseCaccioppoliLocalCanonicalFun_subset_localClosedCube {d : ℕ} {Q : TriadicCube d} {center : Vec d} {rhoInner rhoOuter : ℝ} (hinner : 0 < rhoInner) (hinnerOuter : rhoInner < rhoOuter) : Function.support (scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter)) ⊆ coarseCaccioppoliLocalClosedCube Q center rhoOuter

theorem HCPolySupport.scalarCutoffGradientField_coarseCaccioppoliLocalCanonicalFun_eq_zero_of_notMem_localClosedCube {d : ℕ} {Q : TriadicCube d} {center : Vec d} {rhoInner rhoOuter : ℝ} (hinner : 0 < rhoInner) (hinnerOuter : rhoInner < rhoOuter) {x : Vec d} (hx : x ∉ coarseCaccioppoliLocalClosedCube Q center rhoOuter) : scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter) x = 0

theorem HCPolySupport.coarseCaccioppoliLocalCanonicalFun_gradient_bound {d : ℕ} (Q : TriadicCube d) (center : Vec d) {rhoInner rhoOuter : ℝ} (hinner : 0 < rhoInner) (hinnerOuter : rhoInner < rhoOuter) (x : Vec d) : ‖fderiv ℝ (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter) x‖ ≤ quantitativeCubeCutoffGradientConst d / ((rhoOuter - rhoInner) * (cubeRadius Q / 3))

theorem HCPolySupport.coarseCaccioppoliLocalCanonicalFun_hessian_bound {d : ℕ} (Q : TriadicCube d) (center : Vec d) {rhoInner rhoOuter : ℝ} (hinner : 0 < rhoInner) (hinnerOuter : rhoInner < rhoOuter) (x : Vec d) : ‖iteratedFDeriv ℝ 2 (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter) x‖ ≤ quantitativeCubeCutoffHessianConst d / ((rhoOuter - rhoInner) * (cubeRadius Q / 3)) ^ 2

theorem HCPolySupport.coarseCaccioppoliLocalCanonicalFun_memLp_top_gradientField_on_cube {d : ℕ} (Q R : TriadicCube d) (center : Vec d) {rhoInner rhoOuter : ℝ} (hinner : 0 < rhoInner) (hinnerOuter : rhoInner < rhoOuter) : MeasureTheory.MemLp (scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter)) ⊤ (normalizedCubeMeasure R)

theorem HCPolySupport.coarseCaccioppoliLocalCanonicalFun_cubeLpNorm_infty_gradientField_le_on_cube {d : ℕ} (Q R : TriadicCube d) (center : Vec d) {rhoInner rhoOuter : ℝ} (hinner : 0 < rhoInner) (hinnerOuter : rhoInner < rhoOuter) : cubeLpNorm R ⊤ (scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter)) ≤ quantitativeCubeCutoffGradientConst d / ((rhoOuter - rhoInner) * (cubeRadius Q / 3))

theorem HCPolySupport.coarseCaccioppoliLocalCanonicalFun_component_fderiv_bound_on_cubeSet {d : ℕ} (Q R : TriadicCube d) (center : Vec d) {rhoInner rhoOuter : ℝ} (hinner : 0 < rhoInner) (hinnerOuter : rhoInner < rhoOuter) (i : Fin d) (z : Vec d) : z ∈ cubeSet R → ‖fderiv ℝ (fun (x : Vec d) => scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter) x i) z‖ ≤ quantitativeCubeCutoffHessianConst d / ((rhoOuter - rhoInner) * (cubeRadius Q / 3)) ^ 2

theorem HCPolySupport.CoarseCaccioppoliVectorCutoffControls.of_localCanonicalCutoff_on_cube {d : ℕ} (Q R : TriadicCube d) (center : Vec d) (s : ℝ) {rhoInner rhoOuter : ℝ} (hinner : 0 < rhoInner) (hinnerOuter : rhoInner < rhoOuter) (u : Vec d → ℝ) (G : Vec d → Vec d) (energy : Vec d → ℝ) {Acirc1 AcircS C : ℝ} (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)) : CoarseCaccioppoliVectorCutoffControls R s u G (scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter)) energy Acirc1 AcircS (quantitativeCubeCutoffHessianConst d / ((rhoOuter - rhoInner) * (cubeRadius Q / 3)) ^ 2) C