Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch01.Theorems.CircDomination

Coarse-graining support: Support.Book.Ch01.Theorems.CircDomination #

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

Chapter 1 circ domination #

The Chapter 1 public facade consists of the six exact source-regime bounds below. The former totalized-real, disjoint-cube comparisons remain available only as compatibility results in Book.Ch01.Legacy.

source
theorem HCPolySupport.Book.Ch01.dualNegativeBesovQOneHattedSeminorm_le_circNegativeBesovFiniteSeminorm {d : ℕ} (P : DualNegativeBesovQOneParameters) (Q : Cube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) :
dualNegativeBesovQOneHattedSeminorm P Q f hf ≤ 3 ^ (↑d + P.s) * circNegativeBesovFiniteSeminorm (ExactDualQOneParameters.circParameters P) Q f ⋯

In the exact negative q = 1 regime, the hatted dual seminorm is bounded by the exact finite-q circ seminorm. All proof obligations are internal.

source
theorem HCPolySupport.Book.Ch01.dualNegativeBesovQOneFullNorm_le_circNegativeBesovFiniteSeminorm_add_root {d : ℕ} (P : DualNegativeBesovQOneParameters) (Q : Cube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) :
dualNegativeBesovQOneFullNorm P Q f hf ≤ 3 ^ (↑d + P.s) * circNegativeBesovFiniteSeminorm (ExactDualQOneParameters.circParameters P) Q f ⋯ + exactCircDepthWeight Q P.s 0 * ENNReal.ofReal |cubeAverage Q f|

In the exact negative q = 1 regime, the full dual norm is bounded by the exact finite-q circ seminorm plus the literal root term. All proof obligations are internal.

source
theorem HCPolySupport.Book.Ch01.dualNegativeBesovFiniteHattedSeminorm_le_circNegativeBesovFiniteSeminorm {d : ℕ} (P : DualNegativeBesovFiniteParameters) (Q : Cube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) :
dualNegativeBesovFiniteHattedSeminorm P Q f hf ≤ 3 ^ (↑d + P.s) * circNegativeBesovFiniteSeminorm (ExactDualFiniteParameters.circParameters P) Q f ⋯

In the exact finite-interior negative Besov (1 < q < ∞) regime, the hatted dual seminorm is bounded by the exact finite-q circ seminorm. All proof obligations are internal.

source
theorem HCPolySupport.Book.Ch01.dualNegativeBesovFiniteFullNorm_le_circNegativeBesovFiniteSeminorm_add_root {d : ℕ} (P : DualNegativeBesovFiniteParameters) (Q : Cube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) :
dualNegativeBesovFiniteFullNorm P Q f hf ≤ 3 ^ (↑d + P.s) * circNegativeBesovFiniteSeminorm (ExactDualFiniteParameters.circParameters P) Q f ⋯ + exactCircDepthWeight Q P.s 0 * ENNReal.ofReal |cubeAverage Q f|

In the exact finite-interior negative Besov (1 < q < ∞) regime, the full dual norm is bounded by the exact finite-q circ seminorm plus the literal root term. All proof obligations are internal.

source
theorem HCPolySupport.Book.Ch01.dualNegativeBesovTopHattedSeminorm_le_circNegativeBesovTopSeminorm {d : ℕ} (P : DualNegativeBesovTopParameters) (Q : Cube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) :
dualNegativeBesovTopHattedSeminorm P Q f hf ≤ 3 ^ (↑d + P.s) * circNegativeBesovTopSeminorm (ExactDualTopParameters.circParameters P) Q f ⋯

In the exact negative q = ∞ regime, the hatted dual seminorm is bounded by the exact endpoint circ seminorm. All proof obligations are internal.

source
theorem HCPolySupport.Book.Ch01.dualNegativeBesovTopFullNorm_le_circNegativeBesovTopSeminorm_add_root {d : ℕ} (P : DualNegativeBesovTopParameters) (Q : Cube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) :
dualNegativeBesovTopFullNorm P Q f hf ≤ 3 ^ (↑d + P.s) * circNegativeBesovTopSeminorm (ExactDualTopParameters.circParameters P) Q f ⋯ + exactCircDepthWeight Q P.s 0 * ENNReal.ofReal |cubeAverage Q f|

In the exact negative q = ∞ regime, the full dual norm is bounded by the exact endpoint circ seminorm plus the literal root term. All proof obligations are internal.

Legacy totalized-real and disjoint-cube compatibility #

source
theorem HCPolySupport.Book.Ch01.Legacy.circDominatesMeanZeroDualBesov {d : ℕ} (Q : Cube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hs : 0 < s) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hpConjTop : cubeBesovConjExponent p ≠ ⊤) (hq : 1 ≤ q) :
dualNegativeBesovSeminorm Q s p q u ≤ 3 ^ (↑d + s) * circNegativeBesovNorm Q s p q u

Compatibility comparison for the totalized-real, disjoint-cube mean-zero dual Besov seminorm; it is not an exact source-regime theorem.

source
theorem HCPolySupport.Book.Ch01.Legacy.circDominatesFullDualBesov {d : ℕ} (Q : Cube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hs : 0 < s) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hpConjTop : cubeBesovConjExponent p ≠ ⊤) (hq : 1 ≤ q) :
dualNegativeBesovNorm Q s p q u ≤ 3 ^ (↑d + s) * circNegativeBesovNorm Q s p q u + cubeBesovScaleWeight s Q * ‖normalizedAverage Q u‖

Compatibility comparison for the totalized-real, disjoint-cube full dual Besov norm; it is not an exact source-regime theorem.

source
theorem HCPolySupport.Book.Ch01.Legacy.cubeBesovPairing_le_circNorm_of_fullTest {d : ℕ} (Q : Cube d) (s : ℝ) (p q : ENNReal) (u g : Vec d → ℝ) (hs : 0 < s) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hpConjTop : cubeBesovConjExponent p ≠ ⊤) (hq : 1 ≤ q) (hg : CubeBesovDualFullTest Q s p q g) :
|cubeBesovPairing Q u g| ≤ 3 ^ (↑d + s) * circNegativeBesovNorm Q s p q u

Compatibility pairing estimate for totalized-real, disjoint-cube Besov quantities and unit full-dual positive tests; it is not an exact source pairing theorem.