Coarse-graining support: Support.Deterministic.CoarsePoincare.QOne

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

theorem HCPolySupport.cubeBesovNegativeVectorDepthAverage_le_gradientEnergy {d : ℕ} {Q : TriadicCube d} (a : CoeffField d) (g : Vec d → Vec d) (energy : Vec d → ℝ) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hgrad : CubeAverageGradientEnergyControl Q a g energy) (j : ℕ) : cubeBesovNegativeVectorDepthAverage Q g j ≤ maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑j) a * cubeAverage Q energy

theorem HCPolySupport.cubeBesovNegativeVectorDepthAverage_le_fluxEnergy {d : ℕ} {Q : TriadicCube d} (a : CoeffField d) (flux : Vec d → Vec d) (energy : Vec d → ℝ) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hflux : CubeAverageFluxEnergyControl Q a flux energy) (j : ℕ) : cubeBesovNegativeVectorDepthAverage Q flux j ≤ maxDescendantBBlockNormAtScale Q (Q.scale - ↑j) a * cubeAverage Q energy

theorem HCPolySupport.coarsePoincare_gradient_qone_of_cubeAverageEnergyControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (hs : 0 < s) (g : Vec d → Vec d) (energy : Vec d → ℝ) (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)) : cubeBesovNegativeVectorSeminorm Q s g ≤ (geometricDiscount s 1)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (-1 / 2) * √(cubeAverage Q energy)

theorem HCPolySupport.coarsePoincare_flux_qone_of_cubeAverageEnergyControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (hs : 0 < s) (flux : Vec d → Vec d) (energy : Vec d → ℝ) (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)) : cubeBesovNegativeVectorSeminorm Q s flux ≤ (geometricDiscount s 1)⁻¹ * (LambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (1 / 2) * √(cubeAverage Q energy)

theorem HCPolySupport.coarsePoincare_qone_note_bounds_of_cubeAverageEnergyControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (hs : 0 < s) (g flux : Vec d → Vec d) (energy : Vec d → ℝ) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hgrad : CubeAverageGradientEnergyControl Q a g energy) (hflux : CubeAverageFluxEnergyControl Q a flux energy) (hsum_grad : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hsum_flux : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : cubeBesovNegativeVectorSeminorm Q s g ≤ (geometricDiscount s 1)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (-1 / 2) * √(cubeAverage Q energy) ∧ cubeBesovNegativeVectorSeminorm Q s flux ≤ (geometricDiscount s 1)⁻¹ * (LambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (1 / 2) * √(cubeAverage Q energy)

Note-facing q = 1 gradient and flux coarse Poincare bounds under direct descendant cube-average energy control.

theorem HCPolySupport.coarsePoincare_qone_note_bounds_of_aHarmonicFunction {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) {lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (u : AHarmonicFunction a (cubeSet Q)) : (cubeBesovNegativeVectorSeminorm Q s fun (x : Vec d) => u.toH1.grad x) ≤ (geometricDiscount s 1)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (-1 / 2) * √(cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a u x) ∧ (cubeBesovNegativeVectorSeminorm Q s fun (x : Vec d) => matVecMul (a x) (u.toH1.grad x)) ≤ (geometricDiscount s 1)⁻¹ * (LambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (1 / 2) * √(cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a u x)

Note-facing q = 1 gradient and flux coarse Poincare bounds for one harmonic field on the parent cube.