Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch03.Theorems.CoarsePoincare.NegativeBesov

Coarse-graining support: Support.Book.Ch03.Theorems.CoarsePoincare.NegativeBesov #

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

Section 3.1.1: Coarse Poincare negative-Besov bridges #

This file contains the negative-Besov normalization and pointwise coefficient bridges used by the public coarse Poincare theorem package.

source
theorem HCPolySupport.Book.Ch03.negativeBesovVectorDepthAverage_eq_old {d : ℕ} (Q : TriadicCube d) (F : Vec d → Vec d) (j : ℕ) :
negativeBesovVectorDepthAverage Q F j = cubeBesovNegativeVectorDepthAverage Q F j
source
theorem HCPolySupport.Book.Ch03.negativeBesovVectorDepthSeminorm_eq_old {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) (j : ℕ) :
negativeBesovVectorDepthSeminorm Q s F j = cubeBesovNegativeVectorDepthSeminorm Q s F j
source
theorem HCPolySupport.Book.Ch03.negativeBesovVectorDepthAverage_nonneg {d : ℕ} (Q : TriadicCube d) (F : Vec d → Vec d) (j : ℕ) :
0 ≤ negativeBesovVectorDepthAverage Q F j
source
theorem HCPolySupport.Book.Ch03.negativeBesovVectorDepthSeminorm_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) (j : ℕ) :
0 ≤ negativeBesovVectorDepthSeminorm Q s F j
source
theorem HCPolySupport.Book.Ch03.negativeBesovVectorPartialNormFinite_nonneg {d : ℕ} (Q : TriadicCube d) (s q : ℝ) (N : ℕ) (F : Vec d → Vec d) :
0 ≤ negativeBesovVectorPartialNormFinite Q s q N F
source
theorem HCPolySupport.Book.Ch03.scaleNormalizedNegativeBesovVectorNorm_finite_le_of_partialBound {d : ℕ} (Q : TriadicCube d) (s q : ℝ) (F : Vec d → Vec d) {B : ℝ} (hB : ∀ (N : ℕ), negativeBesovVectorPartialNormFinite Q s q N F ≤ B) :
scaleNormalizedNegativeBesovVectorNorm Q s (Ch02.MultiscaleExponent.finite q) F ≤ B
source
theorem HCPolySupport.Book.Ch03.scaleNormalizedNegativeBesovVectorNorm_infinity_le_of_depthBound {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) {B : ℝ} (hB : ∀ (j : ℕ), negativeBesovVectorDepthSeminorm Q s F j ≤ B) :
scaleNormalizedNegativeBesovVectorNorm Q s Ch02.MultiscaleExponent.infinity F ≤ B
source
theorem HCPolySupport.Book.Ch03.negativeBesovVectorDepthAverage_eq_of_ae_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {F G : Vec d → Vec d} (hFG : F =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] G) (j : ℕ) :
negativeBesovVectorDepthAverage Q F j = negativeBesovVectorDepthAverage Q G j
source
theorem HCPolySupport.Book.Ch03.negativeBesovVectorDepthSeminorm_eq_of_ae_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {F G : Vec d → Vec d} (s : ℝ) (hFG : F =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] G) (j : ℕ) :
negativeBesovVectorDepthSeminorm Q s F j = negativeBesovVectorDepthSeminorm Q s G j
source
theorem HCPolySupport.Book.Ch03.negativeBesovVectorPartialNormFinite_eq_of_ae_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {F G : Vec d → Vec d} (s q : ℝ) (N : ℕ) (hFG : F =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] G) :
negativeBesovVectorPartialNormFinite Q s q N F = negativeBesovVectorPartialNormFinite Q s q N G
source
theorem HCPolySupport.Book.Ch03.scaleNormalizedNegativeBesovVectorNorm_eq_of_ae_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {F G : Vec d → Vec d} (s : ℝ) (q : Ch02.MultiscaleExponent) (hFG : F =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] G) :
scaleNormalizedNegativeBesovVectorNorm Q s q F = scaleNormalizedNegativeBesovVectorNorm Q s q G
source
theorem HCPolySupport.Book.Ch03.negativeBesovVectorDepthAverage_le_publicSigmaStarInvEnergy {d : ℕ} [NeZero d] {Q : TriadicCube d} (a : CoeffFamily d) (F : Vec d → Vec d) (energy : Vec d → ℝ) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hlocal : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, vecNormSq (cubeAverageVec R F) ≤ Ch02.coarseSigmaStarInvMatrixNorm R a * cubeAverage R energy) (j : ℕ) :
negativeBesovVectorDepthAverage Q F j ≤ Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑j) a * cubeAverage Q energy
source
theorem HCPolySupport.Book.Ch03.negativeBesovVectorDepthAverage_le_publicBEnergy {d : ℕ} [NeZero d] {Q : TriadicCube d} (a : CoeffFamily d) (F : Vec d → Vec d) (energy : Vec d → ℝ) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hlocal : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, vecNormSq (cubeAverageVec R F) ≤ Ch02.coarseBMatrixNorm R a * cubeAverage R energy) (j : ℕ) :
negativeBesovVectorDepthAverage Q F j ≤ Ch02.maxDescendantBMatrixNormAtScale Q (Q.scale - ↑j) a * cubeAverage Q energy
source
theorem HCPolySupport.Book.Ch03.pointwiseCoeffField_isEllipticFieldOn_cubeSet {d : ℕ} (Q : TriadicCube d) (aQ : Ch02.CoeffOn (Ch02.cubeDomain Q)) :
IsEllipticFieldOn aQ.lam aQ.Lam (cubeSet Q) (Internal.Ch02.BookCh02.pointwiseCoeffField (Ch02.cubeDomain Q) aQ)