Documentation

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

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

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

Finite-basis reduction for the quenched unit-vector maximum #

This file records the deterministic finite-dimensional reduction used in Theorem t.homogenization.quenched: because the normalized block response is a nonnegative quadratic form of the full-block vector, the maximum over unit vectors is controlled by finitely many coordinate and pair probes.

source
theorem HCPolySupport.Book.Ch05.Section57.fullBlockQuadratic_vec_smul {d : ℕ} (M : FullBlockMat d) (c : ℝ) (q : FullBlockVec d) :
Section54.VarianceBoundGoodScale.fullBlockQuadratic M (c • q) = c ^ 2 * Section54.VarianceBoundGoodScale.fullBlockQuadratic M q
source
noncomputable def HCPolySupport.Book.Ch05.Section57.limitNormalizedBlockJMatrix {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (Q : TriadicCube d) (a : RegCoeffField d) :
FullBlockMat d

The full-block matrix whose quadratic form is J(Q,\overline A^{-1/2}e,\overline A^{1/2}e).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.Book.Ch05.Section57.limitNormalizedBlockJMatrix_isSymm_of_isSymmetricBlockMat {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {Q : TriadicCube d} {a : RegCoeffField d} (hA : IsSymmetricBlockMat (coarseBlockMatrix (cubeSet Q) a.toFun)) :
    Matrix.IsSymm (limitNormalizedBlockJMatrix hP hStruct Q a)
    source
    theorem HCPolySupport.Book.Ch05.Section57.limitNormalizedBlockJMatrix_isSymm_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (Q : TriadicCube d) :
    ∀ᵐ (a : RegCoeffField d) ∂P, Matrix.IsSymm (limitNormalizedBlockJMatrix hP hStruct Q a)
    source
    theorem HCPolySupport.Book.Ch05.Section57.limitNormalizedBlockJMatrix_quadratic_eq_blockJQuadratic {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) (Q : TriadicCube d) (e : FullBlockVec d) (a : RegCoeffField d) :
    Section54.VarianceBoundGoodScale.fullBlockQuadratic (limitNormalizedBlockJMatrix hP hStruct Q a) e = Ch04.blockJQuadraticFullBlockMat (toFullBlockMat (coarseBlockMatrix (cubeSet Q) a.toFun)) (scalarLimitInvSqrtBlockVec hP hStruct e) (scalarLimitSqrtBlockVec hP hStruct e)
    source
    theorem HCPolySupport.Book.Ch05.Section57.limitNormalizedBlockJObservable_ae_eq_limitNormalizedBlockJMatrix_quadratic {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) (Q : TriadicCube d) (e : FullBlockVec d) :
    limitNormalizedBlockJObservable hP hStruct Q e =ᵐ[P] fun (a : RegCoeffField d) => Section54.VarianceBoundGoodScale.fullBlockQuadratic (limitNormalizedBlockJMatrix hP hStruct Q a) e
    source
    theorem HCPolySupport.Book.Ch05.Section57.limitNormalizedBlockJObservable_eq_limitNormalizedBlockJMatrix_quadratic {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) {a : RegCoeffField d} (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (e : FullBlockVec d) :
    limitNormalizedBlockJObservable hP hStruct Q e a = Section54.VarianceBoundGoodScale.fullBlockQuadratic (limitNormalizedBlockJMatrix hP hStruct Q a) e
    source
    theorem HCPolySupport.Book.Ch05.Section57.limitNormalizedBlockJObservable_smul_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) (Q : TriadicCube d) (c : ℝ) (e : FullBlockVec d) :
    limitNormalizedBlockJObservable hP hStruct Q (c • e) =ᵐ[P] fun (a : RegCoeffField d) => c ^ 2 * limitNormalizedBlockJObservable hP hStruct Q e a
    source
    noncomputable def HCPolySupport.Book.Ch05.Section57.limitNormalizedJProbeSum {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (Q : TriadicCube d) :
    RegCoeffField d → ℝ

    Finite coordinate and pair probes for the limiting-normalized J quadratic on one cube.

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

      The normalized finite probe sum: coordinate probes are unchanged, while plus/minus pair probes are scaled by 1/2 so their Euclidean square norm is at most one.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem HCPolySupport.Book.Ch05.Section57.limitNormalizedBlockJObservable_le_probeSum_of_aelocallyUniformlyEllipticField {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) {a : RegCoeffField d} (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (e : FullBlockVec d) (he : e ⬝ᵥ e ≤ 1) :
        limitNormalizedBlockJObservable hP hStruct Q e a ≤ ↑(Fintype.card (BlockCoord d)) * limitNormalizedJProbeSum hP hStruct Q a

        Pointwise finite-basis control for a sampled coefficient field carrying an a.e.-ellipticity witness. This is the simultaneous version needed when the unit-vector supremum is packaged into a Chapter 2 scale response.

        source
        theorem HCPolySupport.Book.Ch05.Section57.limitNormalizedJProbeSum_le_four_normalizedProbeSum_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) (Q : TriadicCube d) :
        limitNormalizedJProbeSum hP hStruct Q ≤ᵐ[P] fun (a : RegCoeffField d) => 4 * limitNormalizedJNormalizedProbeSum hP hStruct Q a
        source
        theorem HCPolySupport.Book.Ch05.Section57.limitNormalizedBlockJObservable_le_probeSum_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) (Q : TriadicCube d) (e : FullBlockVec d) (he : e ⬝ᵥ e ≤ 1) :
        limitNormalizedBlockJObservable hP hStruct Q e ≤ᵐ[P] fun (a : RegCoeffField d) => ↑(Fintype.card (BlockCoord d)) * limitNormalizedJProbeSum hP hStruct Q a
        source
        theorem HCPolySupport.Book.Ch05.Section57.limitNormalizedBlockJObservable_le_normalizedProbeSum_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) (Q : TriadicCube d) (e : FullBlockVec d) (he : e ⬝ᵥ e ≤ 1) :
        limitNormalizedBlockJObservable hP hStruct Q e ≤ᵐ[P] fun (a : RegCoeffField d) => 4 * ↑(Fintype.card (BlockCoord d)) * limitNormalizedJNormalizedProbeSum hP hStruct Q a