Coarse-graining support:

Support.Sobolev.Foundations.CubeCalderonZygmund.HarmonicGradientIterationGeometry

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

Central descendants for the harmonic gradient iteration

This file fixes the ordinary, geometrically central triadic descendants used to iterate the local harmonic gradient gain. They are deliberately distinct from ScalarOverlap.middleChildCube: the latter is an overlap-indexing cube whose carrier remains at the parent scale, whereas the cubes here are genuine members of childCubes and hence contract by a factor of three at every step.

def HCPolySupport.CubeCalderonZygmund.centralChild {d : ℕ} (Q : TriadicCube d) : TriadicCube d

The ordinary central triadic child of Q. Its all-one digit vector makes it a genuine member of childCubes Q, unlike the overlap-centre construction.

Equations

• HCPolySupport.CubeCalderonZygmund.centralChild Q = { scale := Q.scale - 1, index := fun (i : Fin d) => 3 * Q.index i }

def HCPolySupport.CubeCalderonZygmund.centralDescendant {d : ℕ} (Q : TriadicCube d) : ℕ → TriadicCube d

The repeatedly central depth-n descendant used by the CZ iteration.

Equations

• HCPolySupport.CubeCalderonZygmund.centralDescendant Q 0 = Q
• HCPolySupport.CubeCalderonZygmund.centralDescendant Q n.succ = HCPolySupport.CubeCalderonZygmund.centralChild (HCPolySupport.CubeCalderonZygmund.centralDescendant Q n)

@[simp]

theorem HCPolySupport.CubeCalderonZygmund.centralDescendant_zero {d : ℕ} (Q : TriadicCube d) : centralDescendant Q 0 = Q

@[simp]

theorem HCPolySupport.CubeCalderonZygmund.centralDescendant_succ {d : ℕ} (Q : TriadicCube d) (n : ℕ) : centralDescendant Q (n + 1) = centralChild (centralDescendant Q n)

@[simp]

theorem HCPolySupport.CubeCalderonZygmund.centralChild_scale {d : ℕ} (Q : TriadicCube d) : (centralChild Q).scale = Q.scale - 1

theorem HCPolySupport.CubeCalderonZygmund.centralChild_mem_childCubes {d : ℕ} (Q : TriadicCube d) : centralChild Q ∈ childCubes Q

theorem HCPolySupport.CubeCalderonZygmund.centralDescendant_mem_descendantsAtDepth {d : ℕ} (Q : TriadicCube d) (n : ℕ) : centralDescendant Q n ∈ descendantsAtDepth Q n

theorem HCPolySupport.CubeCalderonZygmund.centralDescendant_scale {d : ℕ} (Q : TriadicCube d) (n : ℕ) : (centralDescendant Q n).scale = Q.scale - ↑n

theorem HCPolySupport.CubeCalderonZygmund.centralDescendant_index {d : ℕ} (Q : TriadicCube d) (n : ℕ) (i : Fin d) : (centralDescendant Q n).index i = 3 ^ n * Q.index i

The index of a central descendant is obtained by multiplying the parent index by the corresponding triadic power.

theorem HCPolySupport.CubeCalderonZygmund.centralDescendant_originCube_zero_eq_originCube_neg_nat {d : ℕ} (n : ℕ) : centralDescendant (originCube d 0) n = originCube d (-↑n)

Central descendants of the unit centered cube are precisely the centered triadic cubes at the corresponding negative depth.

theorem HCPolySupport.CubeCalderonZygmund.centralDescendant_cubeScaleFactor {d : ℕ} (Q : TriadicCube d) (n : ℕ) : cubeScaleFactor (centralDescendant Q n) = cubeScaleFactor Q / 3 ^ n

theorem HCPolySupport.CubeCalderonZygmund.centralDescendant_cubeVolume_eq {d : ℕ} (Q : TriadicCube d) (n : ℕ) : cubeVolume Q = ↑((3 ^ d) ^ n) * cubeVolume (centralDescendant Q n)

theorem HCPolySupport.CubeCalderonZygmund.centralDescendant_cubeVolume_ratio {d : ℕ} (Q : TriadicCube d) (n : ℕ) : cubeVolume Q / cubeVolume (centralDescendant Q n) = ↑((3 ^ d) ^ n)

theorem HCPolySupport.CubeCalderonZygmund.centralDescendant_cubeSet_subset {d : ℕ} (Q : TriadicCube d) (n : ℕ) : cubeSet (centralDescendant Q n) ⊆ cubeSet Q

theorem HCPolySupport.CubeCalderonZygmund.centralDescendant_openCubeSet_subset {d : ℕ} (Q : TriadicCube d) (n : ℕ) : openCubeSet (centralDescendant Q n) ⊆ openCubeSet Q

theorem HCPolySupport.CubeCalderonZygmund.centralChild_cubeSet_subset_scaledOpenInnerHalf {d : ℕ} (Q : TriadicCube d) : cubeSet (centralChild Q) ⊆ scaledOpenCubeSet Q (1 / 2)

One central child lies strictly inside the half-sized open cube of its parent. This is the geometric margin consumed at every harmonic-gain step.

theorem HCPolySupport.CubeCalderonZygmund.centralDescendant_succ_cubeSet_subset_scaledOpenInnerHalf {d : ℕ} (Q : TriadicCube d) (n : ℕ) : cubeSet (centralDescendant Q (n + 1)) ⊆ scaledOpenCubeSet (centralDescendant Q n) (1 / 2)

The central step at depth n lies in the strict inner half of its depth n predecessor, so the harmonic regularity engine can be iterated.

theorem HCPolySupport.CubeCalderonZygmund.normalizedCubeMeasure_centralDescendant_eq_smul_restrict {d : ℕ} (Q : TriadicCube d) (n : ℕ) : normalizedCubeMeasure (centralDescendant Q n) = ENNReal.ofReal ↑((3 ^ d) ^ n) • (normalizedCubeMeasure Q).restrict (cubeSet (centralDescendant Q n))

Exact normalized-measure restriction formula for the central descendant. The factor is the number of ordinary depth-n descendants.

theorem HCPolySupport.CubeCalderonZygmund.eLpNorm_centralDescendant_eq_rpow_smul_restrict {d : ℕ} (Q : TriadicCube d) (n : ℕ) (p : FiniteLpExponent) (f : Vec d → ℝ) : MeasureTheory.eLpNorm f p.exponent (normalizedCubeMeasure (centralDescendant Q n)) = ENNReal.ofReal ↑((3 ^ d) ^ n) ^ (1 / p.exponent).toReal * MeasureTheory.eLpNorm f p.exponent ((normalizedCubeMeasure Q).restrict (cubeSet (centralDescendant Q n)))

The corresponding exact Lᵖ restriction formula.

theorem HCPolySupport.CubeCalderonZygmund.eLpNorm_centralDescendant_le_descendantCount_mul {d : ℕ} (Q : TriadicCube d) (n : ℕ) (p : FiniteLpExponent) (f : Vec d → ℝ) : MeasureTheory.eLpNorm f p.exponent (normalizedCubeMeasure (centralDescendant Q n)) ≤ ENNReal.ofReal ↑((3 ^ d) ^ n) * MeasureTheory.eLpNorm f p.exponent (normalizedCubeMeasure Q)

Restricting from a normalized cube to a central depth-n descendant has at most the descendant-count loss. The exact p-dependent root factor is available in eLpNorm_centralDescendant_eq_rpow_smul_restrict; this coarser form is convenient for the iteration bookkeeping.

theorem HCPolySupport.CubeCalderonZygmund.memLp_centralDescendant_of_memLp {d : ℕ} {Q : TriadicCube d} {p : ENNReal} {f : Vec d → ℝ} (n : ℕ) (hf : MeasureTheory.MemLp f p (normalizedCubeMeasure Q)) : MeasureTheory.MemLp f p (normalizedCubeMeasure (centralDescendant Q n))

Finite Lᵖ data on a cube restricts to every central descendant.

theorem HCPolySupport.CubeCalderonZygmund.eLpNorm_centralDescendant_downgrade_le {d : ℕ} (Q : TriadicCube d) (n : ℕ) (p : FiniteLpExponent) (hp : p.exponent ≤ 2) (f : Vec d → ℝ) (hf : MeasureTheory.AEStronglyMeasurable f (normalizedCubeMeasure (centralDescendant Q n))) : MeasureTheory.eLpNorm f p.exponent (normalizedCubeMeasure (centralDescendant Q n)) ≤ MeasureTheory.eLpNorm f 2 (normalizedCubeMeasure (centralDescendant Q n))

On the probability-normalized central descendant, every finite exponent below 2 is bounded by the L² norm without a volume loss.