Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch05.Theorems.Section57.LocalizedFiniteBasis

Coarse-graining support: Support.Book.Ch05.Theorems.Section57.LocalizedFiniteBasis #

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

Localized finite-basis reduction #

This file upgrades the one-cube finite-basis reduction to the finite maximum over the scale-n descendants of the scale-m origin cube.

source
noncomputable def HCPolySupport.Book.Ch05.Section57.localizedLimitNormalizedJProbeSumMax {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m n : ℕ) :
RegCoeffField d → ℝ

The finite maximum, over descendants, of the coordinate/pair probe sum controlling the limiting-normalized quadratic form.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def HCPolySupport.Book.Ch05.Section57.localizedLimitNormalizedJNormalizedProbeSumMax {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m n : ℕ) :
    RegCoeffField d → ℝ

    The localized maximum of the normalized coordinate/pair probe sum.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.Book.Ch05.Section57.limitNormalizedJProbeSum_le_localizedLimitNormalizedJProbeSumMax {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {m n : ℕ} {R : TriadicCube d} (hR : R ∈ descendantsAtScale (originCube d ↑m) ↑n) (a : RegCoeffField d) :
      limitNormalizedJProbeSum hP hStruct R a ≤ localizedLimitNormalizedJProbeSumMax hP hStruct m n a
      source
      theorem HCPolySupport.Book.Ch05.Section57.localizedLimitNormalizedJMax_le_probeSumMax_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) {m n : ℕ} (hnm : n ≤ m) (e : FullBlockVec d) (he : e ⬝ᵥ e ≤ 1) :
      localizedLimitNormalizedJMax hP hStruct m n e ≤ᵐ[P] fun (a : RegCoeffField d) => ↑(Fintype.card (BlockCoord d)) * localizedLimitNormalizedJProbeSumMax hP hStruct m n a

      The localized maximum over any fixed unit vector is a.s. controlled by the localized finite-probe maximum. This is the Lean form of the finite-basis reduction used in Theorem t.homogenization.quenched.

      source
      theorem HCPolySupport.Book.Ch05.Section57.localizedLimitNormalizedJMax_le_normalizedProbeSumMax_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) {m n : ℕ} (hnm : n ≤ m) (e : FullBlockVec d) (he : e ⬝ᵥ e ≤ 1) :
      localizedLimitNormalizedJMax hP hStruct m n e ≤ᵐ[P] fun (a : RegCoeffField d) => 4 * ↑(Fintype.card (BlockCoord d)) * localizedLimitNormalizedJNormalizedProbeSumMax hP hStruct m n a
      source
      theorem HCPolySupport.Book.Ch05.Section57.localizedLimitNormalizedJMax_smul_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) {m n : ℕ} (hnm : n ≤ m) (c : ℝ) (hc : c ≠ 0) (e : FullBlockVec d) :
      localizedLimitNormalizedJMax hP hStruct m n (c • e) =ᵐ[P] fun (a : RegCoeffField d) => c ^ 2 * localizedLimitNormalizedJMax hP hStruct m n e a