BlockLocalization

BlockLocalization

Square-block support decomposition and leakage. Scaffolding notes: ScaffoldingNotes/Blocks/block_localization.md.

theorem Hermite1DimdLEAN.blockDecompositionNorm {d : ℕ} (κ : MultiIndex d) (G : FiniteHermiteSum d) : hermiteNormSq κ G = ∑' (ℓ : MultiIndex d), hermiteNormSq κ (blockPart ℓ G)

Orthogonal block decomposition by square blocks.

theorem Hermite1DimdLEAN.explicitLocalAndFarSupport {d : ℕ} (j : MultiIndex d) (M : ℕ) (G : FiniteHermiteSum d) : Disjoint (localCoeffSet j M G) (farCoeffSet j M G) ∧ localCoeffSet j M G ∪ farCoeffSet j M G = G.support ∧ (localPart j M G).support = localCoeffSet j M G ∧ (remainderPart j M G).support = farCoeffSet j M G

Explicit local and far support sets relative to an annulus and width.

theorem Hermite1DimdLEAN.productBasisLocalization {d : ℕ} (κ : MultiIndex d) : ∃ (C : ℝ) (c : ℝ) (B : ℝ), 0 < C ∧ 0 < c ∧ 0 ≤ B ∧ ∀ (α j ℓ : MultiIndex d), α ∈ squareBlock ℓ → annulusMass j (PhiKappaAlpha κ α) ≤ C * Real.exp (-c * max (↑(blockDistance j ℓ) - B) 0 ^ 2)

Single-basis localization on a product annulus.

theorem Hermite1DimdLEAN.blockLocalization {d : ℕ} (κ : MultiIndex d) : ∃ (C : ℝ) (c : ℝ) (B : ℝ), 0 < C ∧ 0 < c ∧ 0 ≤ B ∧ ∀ (j ℓ : MultiIndex d) (G : FiniteHermiteSum d), annulusMass j (evalHermiteSum κ (blockPart ℓ G)) ≤ C * Real.exp (-c * max (↑(blockDistance j ℓ) - B) 0 ^ 2) * hermiteNormSq κ (blockPart ℓ G)

Quantitative block localization estimate.

theorem Hermite1DimdLEAN.shellCountingFormula (d r : ℕ) : (2 * r + 1) ^ d - (2 * r - 1) ^ d ≤ (2 * r + 1) ^ d

Crude shell-count helper for sup-norm block shells.

theorem Hermite1DimdLEAN.polynomialGaussianSeriesSummable (m : ℕ) (c : ℝ) (hc : 0 < c) : Summable fun (r : ℕ) => ↑r ^ m * Real.exp (-c * ↑r ^ 2)

Gaussian tails with polynomial weights are summable.

theorem Hermite1DimdLEAN.finiteLeakage {d : ℕ} (κ : MultiIndex d) : ∃ (C : ℝ) (c : ℝ) (B : ℝ), 0 < C ∧ 0 < c ∧ 0 ≤ B ∧ Filter.Tendsto (fun (M : ℕ) => localizationLeakageCoefficient C c B d M) Filter.atTop (nhds 0) ∧ ∀ (M : ℕ) (G : FiniteHermiteSum d), ∑' (j : MultiIndex d), annulusMass j (evalHermiteSum κ (remainderPart j M G)) ≤ localizationLeakageCoefficient C c B d M * hermiteNormSq κ G

Leakage coefficient tends to zero and controls the global remainder.

theorem Hermite1DimdLEAN.finitePartialLeakage {d : ℕ} (κ : MultiIndex d) : ∃ (C : ℝ) (c : ℝ) (B : ℝ), 0 < C ∧ 0 < c ∧ 0 ≤ B ∧ Filter.Tendsto (fun (M : ℕ) => localizationLeakageCoefficient C c B d M) Filter.atTop (nhds 0) ∧ ∀ (s : Finset (MultiIndex d)) (M : ℕ) (G : FiniteHermiteSum d), ∑ j ∈ s, annulusMass j (evalHermiteSum κ (remainderPart j M G)) ≤ localizationLeakageCoefficient C c B d M * hermiteNormSq κ G

Leakage coefficient tends to zero and controls all finite partial remainder sums.