Documentation

LeanPool.HighContrastHomogenization.Provider.Quenched.SmallContrastPerGenerationRec

High-contrast homogenization: Provider.Quenched.SmallContrastPerGenerationRec #

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The per-generation recursion step, assembled #

Step 4 of, scalar half: the conclusion of exists_account_one_step_entry_of_block_at_level at one generation, together with the metric factor bound and the summed slot bounds, put into the drop-history shape hrec_final_sharp_at_jb_src consumes.

Reading the one-step conclusion at eps = F_t and multiplying by d:

F_t ≤ a·(F_s − F_t) + b_q·F_t² + c_w·W²,
a   = 64·C_pre·d·(3/2 + 1/(4η)),
b_q = 2d(3d+4) + 4·C_pre·d·rowCoefficient,
c_w = 4·C_pre·d,

which is exactly the input of hrec_of_one_step_sharp_at_jb / hrec_final_sharp_at_jb_src. The row value is rowCoefficient · eps² by definition, so it lands in the quadratic slot alongside the centering term — this is the printed accounting in which every eps² coefficient is dimensional or κ-scaled.

source
noncomputable def HCPolySupport.HighContrast.Quenched.rowCoefficient {d : ℕ} (Cd g : ℝ) (mAl : Mat d) (G : ℕ) (s t : ℤ) (kap : ℝ) :
ℝ

The eps²-coefficient of the entry row value.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def HCPolySupport.HighContrast.Quenched.dropCoefficient (d : ℕ) (Cpre eta : ℝ) :
    ℝ

    The drop coefficient of the one-step estimate.

    Equations
    Instances For
      source
      def HCPolySupport.HighContrast.Quenched.quadCoefficient (d : ℕ) (Cpre Crow : ℝ) :
      ℝ

      The quadratic coefficient of the one-step estimate.

      Equations
      Instances For
        source
        def HCPolySupport.HighContrast.Quenched.weakCoefficient (d : ℕ) (Cpre : ℝ) :
        ℝ

        The weak coefficient of the one-step estimate.

        Equations
        Instances For
          source
          theorem HCPolySupport.HighContrast.Quenched.one_step_scalar_shape (d : ℕ) {Cpre eta Crow W hatS hatT : ℝ} (hd0 : 0 ≤ ↑d) (hstep : hatT - 1 ≤ 4 * Cpre * ((3 / 2 + 1 / (4 * eta)) * (16 * ↑d * (hatS - hatT)) + Crow * (↑d * (hatT - 1)) ^ 2 + W ^ 2) + 2 * ((3 * ↑d + 4) * (↑d * (hatT - 1)) ^ 2)) :
          ↑d * (hatT - 1) ≤ dropCoefficient d Cpre eta * (↑d * (hatS - 1) - ↑d * (hatT - 1)) + quadCoefficient d Cpre Crow * (↑d * (hatT - 1)) ^ 2 + weakCoefficient d Cpre * W ^ 2

          The one-step estimate in scalar shape. Multiplying the account's hatted one-step conclusion by d turns it into the input of hrec_of_one_step_sharp_at_jb, with the three coefficients above.