Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch01.Theorems.DualToCircLoss.ProjectionTests

Coarse-graining support: Support.Book.Ch01.Theorems.DualToCircLoss.ProjectionTests #

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

Dual-to-circ projection tests #

Legacy finite-truncation projection-test scaffolding for the totalized-real, disjoint/componentwise compatibility lane. This is distinct from the exact ENNReal overlap/dual/circ kernels.

source
theorem HCPolySupport.Book.Ch01.Legacy.cubeBesovConjExponent_two_ne_zero_dualToCirc :
cubeBesovConjExponent 2 ≠ 0
source
theorem HCPolySupport.Book.Ch01.Legacy.cubeBesovConjExponent_two_ne_top_dualToCirc :
cubeBesovConjExponent 2 ≠ ⊤
source
noncomputable def HCPolySupport.Book.Ch01.Legacy.cubeProjectionPositiveTestCoefficientTwo {d : ℕ} (Q : Cube d) (t : ℝ) (j : ℕ) :
ℝ

Uniform positive test bound for the depth-j cube projection. The bound is independent of the finite test depth N; finer scales contribute zero because the projection is already piecewise constant there.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def HCPolySupport.Book.Ch01.Legacy.cubeProjectionPositiveTestBoundTwo {d : ℕ} (Q : Cube d) (t : ℝ) (j : ℕ) (f : Vec d → ℝ) :
    ℝ

    The L² norm of the depth-j projection multiplied by the finite positive Besov scale coefficient.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.Book.Ch01.Legacy.cubeProjectionPositiveTestCoefficientTwo_nonneg {d : ℕ} (Q : Cube d) (t : ℝ) (j : ℕ) :
      0 ≤ cubeProjectionPositiveTestCoefficientTwo Q t j
      source
      theorem HCPolySupport.Book.Ch01.Legacy.cubeProjectionPositiveTestCoefficientTwo_pos {d : ℕ} (Q : Cube d) (t : ℝ) (j : ℕ) :
      0 < cubeProjectionPositiveTestCoefficientTwo Q t j
      source
      theorem HCPolySupport.Book.Ch01.Legacy.cubeProjectionPositiveTestBoundTwo_eq_coefficient_mul_cubeLpNorm {d : ℕ} (Q : Cube d) (t : ℝ) (j : ℕ) (f : Vec d → ℝ) :
      cubeProjectionPositiveTestBoundTwo Q t j f = cubeProjectionPositiveTestCoefficientTwo Q t j * cubeLpNorm Q 2 (cubeProjection Q j f)
      source
      theorem HCPolySupport.Book.Ch01.Legacy.cubeBesovDualTestNorm_cubeProjection_le_positiveTestBound_two {d : ℕ} (Q : Cube d) (t : ℝ) (j N : ℕ) (f : Vec d → ℝ) :
      cubeBesovDualTestNorm Q t 2 2 N (cubeProjection Q j f) ≤ cubeProjectionPositiveTestBoundTwo Q t j f
      source
      theorem HCPolySupport.Book.Ch01.Legacy.cubeBesovPairing_self_projection_eq_sq_cubeLpNorm_two {d : ℕ} (Q : Cube d) (j : ℕ) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure Q)) :
      cubeBesovPairing Q f (cubeProjection Q j f) = cubeLpNorm Q 2 (cubeProjection Q j f) ^ 2

      Testing a function against its depth-j cube projection returns the normalized L² mass of that projection. This is the scale-test identity used in the lossy true-dual-to-circ comparison.

      source
      theorem HCPolySupport.Book.Ch01.Legacy.sq_cubeLpNorm_projection_le_dualFullNorm_mul_testBound_two {d : ℕ} (Q : Cube d) (t : ℝ) (j : ℕ) (f : Vec d → ℝ) {B : ℝ} (ht : 0 < t) (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure Q)) (hB : 0 < B) (hbound : ∀ (N : ℕ), cubeBesovDualTestNorm Q t 2 2 N (cubeProjection Q j f) ≤ B) :
      cubeLpNorm Q 2 (cubeProjection Q j f) ^ 2 ≤ cubeBesovDualFullNorm Q t 2 2 f * B

      If the depth-j projection of f has positive dual-test norm bounded by B at every finite depth, then its L² mass is controlled by the true dual negative Besov norm of f times B. This is the core lower-bound mechanism behind the lossy true-dual-to-circ comparison; the remaining analytic estimate is the explicit positive-Besov test bound for cubeProjection Q j f.

      source
      theorem HCPolySupport.Book.Ch01.Legacy.sq_cubeLpNorm_projection_le_dualFullNorm_mul_positiveTestBound_two {d : ℕ} (Q : Cube d) (t : ℝ) (j : ℕ) (f : Vec d → ℝ) (ht : 0 < t) (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure Q)) (hL : 0 < cubeLpNorm Q 2 (cubeProjection Q j f)) :
      cubeLpNorm Q 2 (cubeProjection Q j f) ^ 2 ≤ cubeBesovDualFullNorm Q t 2 2 f * cubeProjectionPositiveTestBoundTwo Q t j f

      Concrete scale test lower bound with the projection test norm already estimated.

      source
      theorem HCPolySupport.Book.Ch01.Legacy.cubeLpNorm_projection_le_dualFullNorm_mul_positiveTestCoefficient_two {d : ℕ} (Q : Cube d) (t : ℝ) (j : ℕ) (f : Vec d → ℝ) (ht : 0 < t) (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure Q)) :
      cubeLpNorm Q 2 (cubeProjection Q j f) ≤ cubeBesovDualFullNorm Q t 2 2 f * cubeProjectionPositiveTestCoefficientTwo Q t j

      Linear scale estimate obtained by cancelling the nonzero projected L² norm from the quadratic testing lower bound.

      source
      theorem HCPolySupport.Book.Ch01.Legacy.cubeBesovCircDepthAverage_eq_sq_cubeLpNorm_projection_two {d : ℕ} (Q : Cube d) (j : ℕ) (f : Vec d → ℝ) :
      cubeBesovCircDepthAverage Q 2 f j = cubeLpNorm Q 2 (cubeProjection Q j f) ^ 2