Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch05.Theorems.Section56.SmallContrastAssembly.FinalAssembly

Coarse-graining support: Support.Book.Ch05.Theorems.Section56.SmallContrastAssembly.FinalAssembly #

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

Final constant selection for Lemma l.small.contrast.assembly #

This file owns the final real-algebra assembly of the Section 5.6 small-contrast iteration. The analytic fluctuation-sum estimate is kept as a separate input to the pure algebra lemma so the final theorem can quantify the constant before the law.

source
noncomputable def HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.smallContrastAssemblyRHSAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (C : ℝ) (ell k m : ℕ) (e : Vec d) :
ℝ

The right side in Lemma l.small.contrast.assembly.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.smallContrastAssembly_real_bound {J F tau tail geom thetaM thetaEll CJ C Ktau Kgeom Ktheta : ℝ} (hJ : J ≤ CJ * F + CJ * tau + CJ * tail + CJ * thetaM) (hF : F ≤ Ktau * tau + Kgeom * geom + Ktheta * thetaEll) (hCJ_nonneg : 0 ≤ CJ) (htau_nonneg : 0 ≤ tau) (htail_nonneg : 0 ≤ tail) (hgeom_nonneg : 0 ≤ geom) (hthetaEll_nonneg : 0 ≤ thetaEll) (hthetaM_le : thetaM ≤ thetaEll) (hC_tau : CJ * Ktau + CJ ≤ C) (hC_tail : CJ ≤ C) (hC_geom : CJ * Kgeom ≤ C) (hC_theta : CJ * Ktheta + CJ ≤ C) :
    J ≤ C * tau + C * tail + C * geom + C * thetaEll

    Pure real algebra for the last assembly step.

    source
    theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.thetaAtScale_sub_one_sq_mono_of_le {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {ell m : ℕ} (hellm : ell ≤ m) :
    (thetaAtScale hP hStruct ↑m - 1) ^ 2 ≤ (thetaAtScale hP hStruct ↑ell - 1) ^ 2
    source
    theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.tauAtScale_special_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {k m : ℕ} (hkm : k ≤ m) (e : Vec d) :
    have p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; 0 ≤ tauAtScale P (↑m) (↑k) p_e q_e

    Nonnegativity of the special-direction additivity defect.

    source
    theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.smallContrastAssembly_homogenizationScale_of_fluctuation_bound {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) (Ktau Kgeom Ktheta : ℝ) (hFluct : ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P), Ch04.RestrictionStationaryLaw P → ∀ (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P), hP4.params = params → widetildeThetaAtScale P 0 hP4 ≤ 2 → ∀ (e : Vec d), vecNormSq e = 1 → ∀ {ell k m : ℕ}, ell < k → k < m → have p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; Section53.JUpperBoundCoarseFluctuations.coarseFluctuationFullBlockSumAtScale hP hStruct hP4 k m ≤ Ktau * tauAtScale P (↑m) (↑k) p_e q_e + Kgeom * Real.rpow 3 (-↑d * ↑(k - ell)) + Ktheta * (thetaAtScale hP hStruct ↑ell - 1) ^ 2) :
    ∃ (C : ℝ), 0 < C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P), Ch04.RestrictionStationaryLaw P → ∀ (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P), hP4.params = params → widetildeThetaAtScale P 0 hP4 ≤ 2 → ∀ (e : Vec d), vecNormSq e = 1 → ∀ {ell k m : ℕ}, ell < k → k < m → C ≤ ↑(m - k) → have p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; Ch04.expectedResponseJCubeSet P (originCube d ↑m) p_e q_e ≤ smallContrastAssemblyRHSAtScale hP hStruct hP4 C ell k m e

    Final constant selection, assuming a parameter-uniform estimate on the coarse fluctuation sum. The produced constant is chosen before the law.

    source
    theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.smallContrastAssembly_homogenizationScale {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) :
    ∃ (C : ℝ), 0 < C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P), hP4.params = params → widetildeThetaAtScale P 0 hP4 ≤ 2 → ∀ (e : Vec d), vecNormSq e = 1 → ∀ {ell k m : ℕ}, ell < k → k < m → C ≤ ↑(m - k) → have p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; Ch04.expectedResponseJCubeSet P (originCube d ↑m) p_e q_e ≤ smallContrastAssemblyRHSAtScale hP hStruct hP4 C ell k m e

    Lemma l.small.contrast.assembly, with the constant chosen before the law.