Documentation

LeanPool.HighContrastHomogenization.Support.Deterministic.CoarseCaccioppoli.EnergyBridge.Flux

Coarse-graining support: Support.Deterministic.CoarseCaccioppoli.EnergyBridge.Flux #

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

Energy bridges for coarse Caccioppoli #

This sidecar file connects the local cutoff-product Caccioppoli estimate to the coarse-Poincare energy-control surface, without editing the active Poincare files. The main point is to expose the finite q = 1 flux partial bounds that the local pairing theorem consumes.

source
theorem HCPolySupport.norm_le_sqrt_vecNormSq {d : ℕ} (v : Vec d) :
‖v‖ ≤ √(vecNormSq v)
source
theorem HCPolySupport.norm_cubeAverageVec_le_sqrt_coarseBBlockNorm_mul_cubeAverage_of_fluxEnergyControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (flux : Vec d → Vec d) (energy : Vec d → ℝ) (hflux : CubeAverageFluxEnergyControl Q a flux energy) :
‖cubeAverageVec Q flux‖ ≤ √(coarseBBlockNorm Q a * cubeAverage Q energy)
source
theorem HCPolySupport.norm_cubeAverageVec_le_sqrt_coarseBBlockNorm_mul_sqrt_cubeAverage_of_fluxEnergyControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (flux : Vec d → Vec d) (energy : Vec d → ℝ) (hflux : CubeAverageFluxEnergyControl Q a flux energy) :
‖cubeAverageVec Q flux‖ ≤ √(coarseBBlockNorm Q a) * √(cubeAverage Q energy)
source
theorem HCPolySupport.sqrt_coarseBBlockNorm_le_inv_geometricDiscount_mul_LambdaSq_one_rpow_half {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s : ℝ} (hs : 0 < s) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) :
√(coarseBBlockNorm Q a) ≤ (geometricDiscount s 1)⁻¹ * (LambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (1 / 2)
source
noncomputable def HCPolySupport.coarseCaccioppoliLambdaFactor {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) :
ℝ

Canonical q = 1 coefficient factor used by the Caccioppoli local bridge. It simultaneously bounds the block-average coefficient and the negative Besov flux coefficient once the corresponding geometric series is summable.

Equations
Instances For
    source
    theorem HCPolySupport.coarseCaccioppoliLambdaFactor_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s : ℝ} (hs : 0 ≤ s) :
    0 ≤ coarseCaccioppoliLambdaFactor Q a s
    source
    theorem HCPolySupport.sqrt_coarseBBlockNorm_le_coarseCaccioppoliLambdaFactor {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s : ℝ} (hs : 0 < s) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) :
    √(coarseBBlockNorm Q a) ≤ coarseCaccioppoliLambdaFactor Q a s
    source
    theorem HCPolySupport.coarseCaccioppoli_gradient_qone_partialBound_of_cubeAverageEnergyControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (hs : 0 < s) (g : Vec d → Vec d) (energy : Vec d → ℝ) (N : ℕ) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hgrad : CubeAverageGradientEnergyControl Q a g energy) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) :
    cubeBesovNegativeVectorPartialSeminorm Q s N g ≤ (geometricDiscount s 1)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (-1 / 2) * √(cubeAverage Q energy)

    Finite q = 1 gradient coarse-Poincare bound, exposed in the Caccioppoli bridge namespace so scalar component circ bounds can be built without reopening the active Poincare files.

    source
    theorem HCPolySupport.coarseCaccioppoli_flux_qone_partialBound_of_cubeAverageEnergyControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (hs : 0 < s) (flux : Vec d → Vec d) (energy : Vec d → ℝ) (N : ℕ) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hflux : CubeAverageFluxEnergyControl Q a flux energy) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) :
    cubeBesovNegativeVectorPartialSeminorm Q s N flux ≤ (geometricDiscount s 1)⁻¹ * (LambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (1 / 2) * √(cubeAverage Q energy)

    Finite q = 1 flux coarse-Poincare bound, exposed in the Caccioppoli bridge namespace so the local pairing theorem can consume the exact partial seminorm hypotheses it needs.