Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch05.Theorems.Section54.VarianceBoundGoodScale.BudgetAbsorption

Coarse-graining support: #

Support.Book.Ch05.Theorems.Section54.VarianceBoundGoodScale.BudgetAbsorption

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

Absorbing the refined variance budgets #

This file controls the deterministic scalar budgets that remain after the finite-probe assembly. The key point is that the Rosenthal descendant-average coefficient is a Section 5.2 large-scale root coefficient with exponent β + d / ξ.

source
theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.coordinateProbeRefinedDescendantAverageK_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hdelta_nonneg : 0 ≤ delta) (j : ℕ) :
0 ≤ coordinateProbeRefinedDescendantAverageK hP4 delta j

Coordinate-probe descendant-average budgets are nonnegative.

source
theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.pairProbeRefinedDescendantAverageK_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hdelta_nonneg : 0 ≤ delta) (j : ℕ) :
0 ≤ pairProbeRefinedDescendantAverageK hP4 delta j

Pair-probe descendant-average budgets are nonnegative.

source
@[simp]
theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.dotProduct_coordinateProbe_self {d : ℕ} (α : BlockCoord d) :
fullBlockCoordinateProbe α ⬝ᵥ fullBlockCoordinateProbe α = 1

Coordinate probes have Euclidean square norm 1.

source
theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.dotProduct_plusProbe_self_le_four {d : ℕ} (α β : BlockCoord d) :
fullBlockPlusProbe α β ⬝ᵥ fullBlockPlusProbe α β ≤ 4

Plus probes have Euclidean square norm at most 4.

source
theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.dotProduct_minusProbe_self_le_four {d : ℕ} (α β : BlockCoord d) :
fullBlockMinusProbe α β ⬝ᵥ fullBlockMinusProbe α β ≤ 4

Minus probes have Euclidean square norm at most 4.

source
theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.refinedScalarProbeVarianceBound_le_basic {d : ℕ} {delta K : ℝ} (q : FullBlockVec d) (hdelta_nonneg : 0 ≤ delta) (hdelta_le_one : delta ≤ 1) (hK_nonneg : 0 ≤ K) (hq_le : q ⬝ᵥ q ≤ 4) :
refinedScalarProbeVarianceBound delta q K ≤ 256 * (delta + K + K ^ 2)

A scalar variance budget with probe square norm at most 4 is controlled by the elementary expression δ + K + K^2.

source
theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.coordinateProbeRefinedVarianceBound_le_basic {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hdelta_nonneg : 0 ≤ delta) (hdelta_le_one : delta ≤ 1) (j : ℕ) (α : BlockCoord d) :
coordinateProbeRefinedVarianceBound hP4 delta j α ≤ 256 * (delta + coordinateProbeRefinedDescendantAverageK hP4 delta j + coordinateProbeRefinedDescendantAverageK hP4 delta j ^ 2)

Coordinate scalar budgets obey the uniform elementary bound.

source
theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.plusProbeRefinedVarianceBound_le_basic {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hdelta_nonneg : 0 ≤ delta) (hdelta_le_one : delta ≤ 1) (j : ℕ) (α β : BlockCoord d) :
plusProbeRefinedVarianceBound hP4 delta j α β ≤ 256 * (delta + pairProbeRefinedDescendantAverageK hP4 delta j + pairProbeRefinedDescendantAverageK hP4 delta j ^ 2)

Plus-pair scalar budgets obey the uniform elementary bound.

source
theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.minusProbeRefinedVarianceBound_le_basic {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hdelta_nonneg : 0 ≤ delta) (hdelta_le_one : delta ≤ 1) (j : ℕ) (α β : BlockCoord d) :
minusProbeRefinedVarianceBound hP4 delta j α β ≤ 256 * (delta + pairProbeRefinedDescendantAverageK hP4 delta j + pairProbeRefinedDescendantAverageK hP4 delta j ^ 2)

Minus-pair scalar budgets obey the uniform elementary bound.

source
theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.section52LargeScaleSet_eq_Icc_int (m : ℕ) :
Section52.section52LargeScaleSet m = Finset.image (fun (j : ℕ) => ↑j) (Finset.Icc 1 m)

The Section 5.2 large-scale set is the integer copy of {1, ..., m}.

source
theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.sum_Icc_int_eq_section52LargeScaleSet_sum (m : ℕ) (F : ℤ → ℝ) :
∑ j ∈ Finset.Icc 1 m, F ↑j = ∑ n ∈ Section52.section52LargeScaleSet m, F n

Reindex a finite sum over manuscript scales as a Section 5.2 large-scale sum.

source
theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.section52LargeScaleRootCoeff_sum_le_beta_decay {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) :
have s := section54VarianceBeta hP4 + ↑d / ↑hP4.xi; ∑ n ∈ Section52.section52LargeScaleSet m, Section52.section52LargeScaleRootCoeff d hP4.xi s m n ≤ (2 * Ch04.rosenthalDescendantsAtScaleLpConst d 0 hP4.xi * geometricDiscount s 1 * (geometricDiscount (↑d - s) 1)⁻¹ + 2 * Ch04.rosenthalDescendantsAtScaleSqrtConst d 0 hP4.xi * geometricDiscount s 1 * (geometricDiscount (↑d / 2 + ↑d / ↑hP4.xi - s) 1)⁻¹) * Real.rpow 3 (-section54VarianceBeta hP4 * ↑m)

Sum of the Section 5.2 large-scale root coefficient at the exponent β + d/ξ, where its scale decay is exactly 3^{-β m}.

source
noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.refinedVarianceBasicBudget {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) (delta : ℝ) (j : ℕ) :
ℝ

The scalar budget left after compressing the finite-probe matrix estimate.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.refinedMatrixBudgetConst (d : ℕ) :
    ℝ

    Dimension-only finite-probe constant for the refined variance budget.

    Equations
    Instances For
      source
      theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.refinedMatrixVarianceScaleBound_le_basicBudget {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hdelta_nonneg : 0 ≤ delta) (hdelta_le_one : delta ≤ 1) (j : ℕ) :
      refinedMatrixVarianceScaleBound hP4 delta j ≤ refinedMatrixBudgetConst d * refinedVarianceBasicBudget hP4 delta j

      The per-scale matrix budget is bounded by the compressed scalar budget.