Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.EnergyBridge.LocalizedEnergyProfile

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

Localized energy profiles for coarse Caccioppoli

This file starts the Phase 3 hlower bridge. The LaTeX proof uses a radius profile obtained by averaging the energy over the inner scaled cube. The lemmas here isolate the purely order-theoretic/cutoff part: once F rho is defined as this localized profile, the lower-bound hypothesis follows from the canonical cutoff being 1 on the inner scaled cube and nonnegative elsewhere.

noncomputable def HCPolySupport.coarseCaccioppoliLocalizedEnergyProfile {d : ℕ} (Q : TriadicCube d) (ρ : ℝ) (energy : Vec d → ℝ) : ℝ

Localized cube-average energy over the closed scaled inner cube.

Equations

• HCPolySupport.coarseCaccioppoliLocalizedEnergyProfile Q ρ energy = HCPolySupport.cubeAverage Q ((HCPolySupport.scaledClosedCubeSet Q ρ).indicator energy)

theorem HCPolySupport.integrableOn_indicator_scaledClosedCubeSet_of_integrableOn_cubeSet {d : ℕ} (Q : TriadicCube d) (ρ : ℝ) {energy : Vec d → ℝ} (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) : MeasureTheory.IntegrableOn ((scaledClosedCubeSet Q ρ).indicator energy) (cubeSet Q) MeasureTheory.volume

Indicator localization preserves cube integrability.

theorem HCPolySupport.cubeAverage_indicator_scaledClosedCubeSet_eq_cubeAverage_of_cubeSet_subset {d : ℕ} {Q R : TriadicCube d} (ρ : ℝ) (energy : Vec d → ℝ) (hsub : cubeSet R ⊆ scaledClosedCubeSet Q ρ) : cubeAverage R ((scaledClosedCubeSet Q ρ).indicator energy) = cubeAverage R energy

On a cube contained in the scaled closed cube, the localized indicator has the same cube average as the original energy density.

theorem HCPolySupport.CoarseCaccioppoliFluxEnergyControls.indicator_scaledClosedCubeSet_of_cubeSet_subset {d : ℕ} {Q R : TriadicCube d} (ρ : ℝ) {a : CoeffField d} {s : ℝ} {flux : Vec d → Vec d} {energy : Vec d → ℝ} (hctrl : CoarseCaccioppoliFluxEnergyControls R a s flux energy) (hsub : cubeSet R ⊆ scaledClosedCubeSet Q ρ) : CoarseCaccioppoliFluxEnergyControls R a s flux ((scaledClosedCubeSet Q ρ).indicator energy)

Flux-energy controls may be localized by an outer indicator on a cube contained in the localization region.

theorem HCPolySupport.integrableOn_canonicalCutoff_mul_of_integrableOn_cubeSet {d : ℕ} (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} {energy : Vec d → ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (x : Vec d) => QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂ x * energy x) (cubeSet Q) MeasureTheory.volume

Multiplication by the canonical cutoff preserves cube integrability.

theorem HCPolySupport.cubeAverage_le_cubeAverage_of_le_on {d : ℕ} (Q : TriadicCube d) {f g : Vec d → ℝ} (hf : MeasureTheory.IntegrableOn f (cubeSet Q) MeasureTheory.volume) (hg : MeasureTheory.IntegrableOn g (cubeSet Q) MeasureTheory.volume) (hfg : ∀ x ∈ cubeSet Q, f x ≤ g x) : cubeAverage Q f ≤ cubeAverage Q g

Monotonicity of cubeAverage from a pointwise comparison on the cube.

noncomputable def HCPolySupport.coarseCaccioppoliLocalPatchRadius {d : ℕ} (Q : TriadicCube d) (rho : ℝ) : ℝ

Radius of the note's local Caccioppoli patch x + rho * cu_{m-1} when the parent cube has radius cubeRadius Q.

Equations

• HCPolySupport.coarseCaccioppoliLocalPatchRadius Q rho = rho * (HCPolySupport.cubeRadius Q / 3)

def HCPolySupport.coarseCaccioppoliLocalClosedCube {d : ℕ} (Q : TriadicCube d) (center : Vec d) (rho : ℝ) : Set (Vec d)

Closed local cube used in the boundary Caccioppoli radius profile. Unlike scaledClosedCubeSet, this is centered at the boundary-patch center, not at the parent cube center, and has base scale one triadic level smaller than the parent.

Equations

• HCPolySupport.coarseCaccioppoliLocalClosedCube Q center rho = {y : HCPolySupport.Vec d | ∀ (i : Fin d), |y i - center i| ≤ HCPolySupport.coarseCaccioppoliLocalPatchRadius Q rho}

def HCPolySupport.coarseCaccioppoliLocalOpenCube {d : ℕ} (Q : TriadicCube d) (center : Vec d) (rho : ℝ) : Set (Vec d)

Open local cube used for support cutoffs in the boundary Caccioppoli argument.

Equations

• HCPolySupport.coarseCaccioppoliLocalOpenCube Q center rho = {y : HCPolySupport.Vec d | ∀ (i : Fin d), |y i - center i| < HCPolySupport.coarseCaccioppoliLocalPatchRadius Q rho}

def HCPolySupport.coarseCaccioppoliLocalClosedPatch {d : ℕ} (Q : TriadicCube d) (center : Vec d) (rho : ℝ) : Set (Vec d)

The note-facing local boundary patch: the local cube intersected with the ambient parent cube. For the normalized parent cu_0, this is (center + rho cu_{-1}) ∩ cu_0.

Equations

• HCPolySupport.coarseCaccioppoliLocalClosedPatch Q center rho = HCPolySupport.openCubeSet Q ∩ HCPolySupport.coarseCaccioppoliLocalClosedCube Q center rho

def HCPolySupport.coarseCaccioppoliLocalOpenPatch {d : ℕ} (Q : TriadicCube d) (center : Vec d) (rho : ℝ) : Set (Vec d)

Open version of the local boundary patch.

Equations

• HCPolySupport.coarseCaccioppoliLocalOpenPatch Q center rho = HCPolySupport.openCubeSet Q ∩ HCPolySupport.coarseCaccioppoliLocalOpenCube Q center rho

theorem HCPolySupport.isClosed_coarseCaccioppoliLocalClosedCube {d : ℕ} (Q : TriadicCube d) (center : Vec d) (rho : ℝ) : IsClosed (coarseCaccioppoliLocalClosedCube Q center rho)

theorem HCPolySupport.measurableSet_coarseCaccioppoliLocalClosedCube {d : ℕ} (Q : TriadicCube d) (center : Vec d) (rho : ℝ) : MeasurableSet (coarseCaccioppoliLocalClosedCube Q center rho)

theorem HCPolySupport.measurableSet_coarseCaccioppoliLocalClosedPatch {d : ℕ} (Q : TriadicCube d) (center : Vec d) (rho : ℝ) : MeasurableSet (coarseCaccioppoliLocalClosedPatch Q center rho)

theorem HCPolySupport.coarseCaccioppoliLocalClosedPatch_subset_openCubeSet {d : ℕ} (Q : TriadicCube d) (center : Vec d) (rho : ℝ) : coarseCaccioppoliLocalClosedPatch Q center rho ⊆ openCubeSet Q

theorem HCPolySupport.coarseCaccioppoliLocalOpenCube_subset_closedCube {d : ℕ} (Q : TriadicCube d) (center : Vec d) (rho : ℝ) : coarseCaccioppoliLocalOpenCube Q center rho ⊆ coarseCaccioppoliLocalClosedCube Q center rho

theorem HCPolySupport.coarseCaccioppoliLocalOpenPatch_subset_closedPatch {d : ℕ} (Q : TriadicCube d) (center : Vec d) (rho : ℝ) : coarseCaccioppoliLocalOpenPatch Q center rho ⊆ coarseCaccioppoliLocalClosedPatch Q center rho

noncomputable def HCPolySupport.coarseCaccioppoliLocalEnergyProfile {d : ℕ} (Q : TriadicCube d) (center : Vec d) (rho : ℝ) (energy : Vec d → ℝ) : ℝ

Local-patch cube-average energy profile with the parent-cube normalization used by the deterministic radius-iteration backbone.

Equations

• HCPolySupport.coarseCaccioppoliLocalEnergyProfile Q center rho energy = HCPolySupport.cubeAverage Q ((HCPolySupport.coarseCaccioppoliLocalClosedCube Q center rho).indicator energy)

theorem HCPolySupport.integrableOn_indicator_coarseCaccioppoliLocalClosedCube_of_integrableOn_cubeSet {d : ℕ} (Q : TriadicCube d) (center : Vec d) (rho : ℝ) {energy : Vec d → ℝ} (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) : MeasureTheory.IntegrableOn ((coarseCaccioppoliLocalClosedCube Q center rho).indicator energy) (cubeSet Q) MeasureTheory.volume

Indicator localization to the local closed cube preserves cube integrability.

theorem HCPolySupport.integrableOn_indicator_coarseCaccioppoliLocalClosedPatch_of_integrableOn_cubeSet {d : ℕ} (Q : TriadicCube d) (center : Vec d) (rho : ℝ) {energy : Vec d → ℝ} (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) : MeasureTheory.IntegrableOn ((coarseCaccioppoliLocalClosedPatch Q center rho).indicator energy) (cubeSet Q) MeasureTheory.volume

Indicator localization to the note's local open-parent patch preserves cube integrability.

theorem HCPolySupport.cubeAverage_indicator_coarseCaccioppoliLocalClosedCube_eq_cubeAverage_of_cubeSet_subset {d : ℕ} {Q R : TriadicCube d} (center : Vec d) (rho : ℝ) (energy : Vec d → ℝ) (hsub : cubeSet R ⊆ coarseCaccioppoliLocalClosedCube Q center rho) : cubeAverage R ((coarseCaccioppoliLocalClosedCube Q center rho).indicator energy) = cubeAverage R energy

On a cube contained in the local closed cube, the localized indicator has the same cube average as the original energy density.

theorem HCPolySupport.cubeAverage_indicator_coarseCaccioppoliLocalClosedPatch_eq_cubeAverage_of_cubeSet_subset {d : ℕ} {Q R : TriadicCube d} (center : Vec d) (rho : ℝ) (energy : Vec d → ℝ) (hsub : cubeSet R ⊆ coarseCaccioppoliLocalClosedPatch Q center rho) : cubeAverage R ((coarseCaccioppoliLocalClosedPatch Q center rho).indicator energy) = cubeAverage R energy

On a cube contained in the local Caccioppoli patch, the localized indicator has the same cube average as the original energy density.

theorem HCPolySupport.CoarseCaccioppoliFluxEnergyControls.indicator_coarseCaccioppoliLocalClosedCube_of_cubeSet_subset {d : ℕ} {Q R : TriadicCube d} (center : Vec d) (rho : ℝ) {a : CoeffField d} {s : ℝ} {flux : Vec d → Vec d} {energy : Vec d → ℝ} (hctrl : CoarseCaccioppoliFluxEnergyControls R a s flux energy) (hsub : cubeSet R ⊆ coarseCaccioppoliLocalClosedCube Q center rho) : CoarseCaccioppoliFluxEnergyControls R a s flux ((coarseCaccioppoliLocalClosedCube Q center rho).indicator energy)

Flux-energy controls may be localized by a local-closed-cube indicator on a cube contained in the local cube.

theorem HCPolySupport.CoarseCaccioppoliFluxEnergyControls.indicator_coarseCaccioppoli_of_cubeSubset {d : ℕ} {Q R : TriadicCube d} (center : Vec d) (rho : ℝ) {a : CoeffField d} {s : ℝ} {flux : Vec d → Vec d} {energy : Vec d → ℝ} (hctrl : CoarseCaccioppoliFluxEnergyControls R a s flux energy) (hsub : cubeSet R ⊆ coarseCaccioppoliLocalClosedPatch Q center rho) : CoarseCaccioppoliFluxEnergyControls R a s flux ((coarseCaccioppoliLocalClosedPatch Q center rho).indicator energy)

Flux-energy controls may be localized by a local-patch indicator on a cube contained in the patch.

theorem HCPolySupport.coarseCaccioppoliLocalEnergyProfile_nonneg {d : ℕ} (Q : TriadicCube d) (center : Vec d) (rho : ℝ) {energy : Vec d → ℝ} (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) : 0 ≤ coarseCaccioppoliLocalEnergyProfile Q center rho energy

The local-patch profile is nonnegative when the energy is nonnegative on the parent cube.

theorem HCPolySupport.coarseCaccioppoliLocalEnergyProfile_le_cubeAverage {d : ℕ} (Q : TriadicCube d) (center : Vec d) (rho : ℝ) {energy : Vec d → ℝ} (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) : coarseCaccioppoliLocalEnergyProfile Q center rho energy ≤ cubeAverage Q energy

The local-patch profile is bounded above by the full parent-cube average.

noncomputable def HCPolySupport.coarseCaccioppoliLocalEnergyRadiusProfile {d : ℕ} (Q : TriadicCube d) (center : Vec d) (energy : Vec d → ℝ) : ℝ → ℝ

Unary radius profile for the note's arbitrary-center local patch.

Equations

• HCPolySupport.coarseCaccioppoliLocalEnergyRadiusProfile Q center energy rho = HCPolySupport.coarseCaccioppoliLocalEnergyProfile Q center rho energy

theorem HCPolySupport.coarseCaccioppoliLocalEnergyRadiusProfile_nonneg {d : ℕ} (Q : TriadicCube d) (center : Vec d) {energy : Vec d → ℝ} (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) ⦃rho : ℝ⦄ : 1 / 3 ≤ rho → rho ≤ 1 → 0 ≤ coarseCaccioppoliLocalEnergyRadiusProfile Q center energy rho

The arbitrary-center local radius profile supplies the nonnegativity hypothesis used by radius iteration.

theorem HCPolySupport.coarseCaccioppoliLocalEnergyRadiusProfile_boundedAbove {d : ℕ} (Q : TriadicCube d) (center : Vec d) {energy : Vec d → ℝ} (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) : CoarseCaccioppoliRadiusBoundedAbove (coarseCaccioppoliLocalEnergyRadiusProfile Q center energy)

The arbitrary-center local radius profile is bounded above by the full parent-cube energy average.

theorem HCPolySupport.coarseCaccioppoliLocalizedEnergyProfile_le_canonicalCutoffEnergy {d : ℕ} (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} (energy : Vec d → ℝ) (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (hprofile_int : MeasureTheory.IntegrableOn ((scaledClosedCubeSet Q ρ₁).indicator energy) (cubeSet Q) MeasureTheory.volume) (hweighted_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂ x * energy x) (cubeSet Q) MeasureTheory.volume) : coarseCaccioppoliLocalizedEnergyProfile Q ρ₁ energy ≤ cubeAverage Q fun (x : Vec d) => QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂ x * energy x

The localized inner energy is bounded by the canonical cutoff-weighted energy. This is the reusable core of the eventual hlower discharge.

theorem HCPolySupport.coarseCaccioppoliLocalizedEnergyProfile_le_canonicalCutoffEnergy_of_integrable {d : ℕ} (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} (energy : Vec d → ℝ) (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) : coarseCaccioppoliLocalizedEnergyProfile Q ρ₁ energy ≤ cubeAverage Q fun (x : Vec d) => QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂ x * energy x

Integrability-free localized-energy lower bound using the canonical cutoff.

theorem HCPolySupport.coarseCaccioppoliLocalizedEnergyProfile_nonneg {d : ℕ} (Q : TriadicCube d) (ρ : ℝ) {energy : Vec d → ℝ} (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) : 0 ≤ coarseCaccioppoliLocalizedEnergyProfile Q ρ energy

The localized profile is nonnegative when the energy is nonnegative on the cube.

theorem HCPolySupport.coarseCaccioppoliLocalizedEnergyProfile_le_cubeAverage {d : ℕ} (Q : TriadicCube d) (ρ : ℝ) {energy : Vec d → ℝ} (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) : coarseCaccioppoliLocalizedEnergyProfile Q ρ energy ≤ cubeAverage Q energy

The localized profile is bounded above by the full cube average.

noncomputable def HCPolySupport.coarseCaccioppoliLocalizedEnergyRadiusProfile {d : ℕ} (Q : TriadicCube d) (energy : Vec d → ℝ) : ℝ → ℝ

Unary radius profile obtained by localizing a fixed energy density.

Equations

• HCPolySupport.coarseCaccioppoliLocalizedEnergyRadiusProfile Q energy ρ = HCPolySupport.coarseCaccioppoliLocalizedEnergyProfile Q ρ energy

theorem HCPolySupport.coarseCaccioppoliLocalizedEnergyRadiusProfile_nonneg {d : ℕ} (Q : TriadicCube d) {energy : Vec d → ℝ} (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) ⦃ρ : ℝ⦄ : 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ coarseCaccioppoliLocalizedEnergyRadiusProfile Q energy ρ

The fixed-energy localized radius profile supplies the nonnegativity hypothesis used by radius iteration.

theorem HCPolySupport.coarseCaccioppoliLocalizedEnergyRadiusProfile_boundedAbove {d : ℕ} (Q : TriadicCube d) {energy : Vec d → ℝ} (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) : CoarseCaccioppoliRadiusBoundedAbove (coarseCaccioppoliLocalizedEnergyRadiusProfile Q energy)

The fixed-energy localized radius profile is bounded above by the full cube energy average.

def HCPolySupport.CoarseCaccioppoliLocalizedEnergyProfileLowerControls {d : ℕ} (Q : TriadicCube d) (F : ℝ → ℝ) (energy : ℝ → ℝ → Vec d → ℝ) : Prop

A concrete localized-radius profile control, stated at the exact arity of the Caccioppoli radius bridge.

Equations

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

theorem HCPolySupport.CoarseCaccioppoliLocalizedEnergyProfileLowerControls.to_canonicalCutoffLower {d : ℕ} {Q : TriadicCube d} {F : ℝ → ℝ} {energy : ℝ → ℝ → Vec d → ℝ} (hprofile : CoarseCaccioppoliLocalizedEnergyProfileLowerControls Q F energy) (henergy_nonneg : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∀ x ∈ cubeSet Q, 0 ≤ energy ρ₁ ρ₂ x) (henergy_int : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.IntegrableOn (energy ρ₁ ρ₂) (cubeSet Q) MeasureTheory.volume) ⦃ρ₁ ρ₂ : ℝ⦄ : 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → F ρ₁ ≤ cubeAverage Q fun (x : Vec d) => QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂ x * energy ρ₁ ρ₂ x

Localized-radius profile controls produce the exact hlower family needed by the weak-testing bridge.

theorem HCPolySupport.CoarseCaccioppoliLocalizedEnergyProfileLowerControls.of_fixedEnergy_le_pairEnergy {d : ℕ} (Q : TriadicCube d) {baseEnergy : Vec d → ℝ} {pairEnergy : ℝ → ℝ → Vec d → ℝ} (hbase_int : MeasureTheory.IntegrableOn baseEnergy (cubeSet Q) MeasureTheory.volume) (hpair_int : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.IntegrableOn (pairEnergy ρ₁ ρ₂) (cubeSet Q) MeasureTheory.volume) (hpoint : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∀ x ∈ scaledClosedCubeSet Q ρ₁, baseEnergy x ≤ pairEnergy ρ₁ ρ₂ x) : CoarseCaccioppoliLocalizedEnergyProfileLowerControls Q (coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy) pairEnergy

Build localized lower controls for a fixed radius profile from a pointwise comparison with the pair-dependent energy on each inner cube.

theorem HCPolySupport.CoarseCaccioppoliLocalizedEnergyProfileLowerControls.of_fixedEnergy_eq_pairEnergy {d : ℕ} (Q : TriadicCube d) {baseEnergy : Vec d → ℝ} {pairEnergy : ℝ → ℝ → Vec d → ℝ} (hbase_int : MeasureTheory.IntegrableOn baseEnergy (cubeSet Q) MeasureTheory.volume) (hpair_int : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.IntegrableOn (pairEnergy ρ₁ ρ₂) (cubeSet Q) MeasureTheory.volume) (hpoint : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∀ x ∈ scaledClosedCubeSet Q ρ₁, baseEnergy x = pairEnergy ρ₁ ρ₂ x) : CoarseCaccioppoliLocalizedEnergyProfileLowerControls Q (coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy) pairEnergy

Equality on each inner cube is a convenient way to supply the fixed-profile lower-control comparison.