Coarse-graining support: Support.Book.Ch05.Definitions

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

Chapter 5 definitions reboot

This file is the active Chapter 5 definition surface. Add definitions here only when they are manuscript-facing and not merely proof plumbing.

structure HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticityParams (d : ℕ) : Type

The parameter-only part of the Chapter 5 quantitative coarse-grained ellipticity input (P4).

This record remembers only the manuscript parameters and inequalities for s_1, s_2, and \xi; it deliberately contains no law-specific integrability data. It is useful for stating constants with the manuscript dependency C(d,s_1,s_2,\xi).

• sUpper : ℝ

  The upper regularity exponent s_1 in the quantitative coarse-grained ellipticity parameters.

• sLower : ℝ

  The lower regularity exponent s_2 in the quantitative coarse-grained ellipticity parameters.

• xi : ℕ

  The integer moment exponent constrained to exceed twice the dimension in (P4).

• two_le_dim : 2 ≤ d
• sUpper_nonneg : 0 ≤ self.sUpper
• sUpper_lt_one : self.sUpper < 1
• sLower_nonneg : 0 ≤ self.sLower
• sLower_lt_one : self.sLower < 1
• xi_gt_two_mul_dim : 2 * ↑d < ↑self.xi
• sum_lt_one : self.sUpper + self.sLower < 1
• dim_div_xi_lt_min : ↑d / ↑self.xi < min self.sUpper self.sLower

theorem HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticityParams.xi_pos {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : 0 < params.xi

The exponent xi in the parameter-only (P4) data is positive.

theorem HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticityParams.two_le_xi {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : 2 ≤ params.xi

The exponent xi in the parameter-only (P4) data is at least two.

theorem HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticityParams.sUpper_pos {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : 0 < params.sUpper

The upper regularity exponent in the parameter-only (P4) data is positive.

theorem HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticityParams.sLower_pos {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : 0 < params.sLower

The lower regularity exponent in the parameter-only (P4) data is positive.

theorem HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticityParams.dim_div_xi_lt_sUpper {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : ↑d / ↑params.xi < params.sUpper

The parameter-only (P4) lower endpoint gives d / xi < sUpper.

theorem HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticityParams.dim_div_xi_lt_sLower {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : ↑d / ↑params.xi < params.sLower

The parameter-only (P4) lower endpoint gives d / xi < sLower.

structure HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity {d : ℕ} [NeZero d] (P : Ch04.RestrictionCoeffLaw d) : Type

The Chapter 5 quantitative coarse-grained ellipticity input (P4).

The fields sUpper, sLower, and xi are the manuscript parameters s_1, s_2, and \xi. The last two fields encode finiteness of the unit-cube moments in (P4) as integrability of the corresponding powers.

• sUpper : ℝ

  The regularity exponent s_1 used in the upper coarse-grained ellipticity moment.

• sLower : ℝ

  The regularity exponent s_2 used in the inverse lower coarse-grained ellipticity moment.

• xi : ℕ

  The common integer power whose upper and inverse lower unit-cube moments are integrable.

• two_le_dim : 2 ≤ d
• sUpper_nonneg : 0 ≤ self.sUpper
• sUpper_lt_one : self.sUpper < 1
• sLower_nonneg : 0 ≤ self.sLower
• sLower_lt_one : self.sLower < 1
• xi_gt_two_mul_dim : 2 * ↑d < ↑self.xi
• sum_lt_one : self.sUpper + self.sLower < 1
• dim_div_xi_lt_min : ↑d / ↑self.xi < min self.sUpper self.sLower
• upper_moment_integrable : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Ch04.LambdaSqCoeffField (originCube d 0) self.sUpper (Ch02.MultiscaleExponent.finite 1) a ^ self.xi) P
• lower_inv_moment_integrable : MeasureTheory.Integrable (fun (a : RegCoeffField d) => (Ch04.lambdaSqCoeffField (originCube d 0) self.sLower (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ^ self.xi) P

def HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity.params {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : QuantitativeCoarseGrainedEllipticityParams d

Forget the law-specific integrability part of (P4), retaining only the manuscript parameters and inequalities.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity.params_sUpper {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : hP4.params.sUpper = hP4.sUpper

@[simp]

theorem HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity.params_sLower {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : hP4.params.sLower = hP4.sLower

@[simp]

theorem HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity.params_xi {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : hP4.params.xi = hP4.xi

theorem HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity.xi_pos {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : 0 < hP4.xi

The exponent xi in (P4) is positive.

theorem HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity.two_le_xi {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : 2 ≤ hP4.xi

The exponent xi in (P4) is at least two.

theorem HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity.sUpper_pos {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : 0 < hP4.sUpper

The upper regularity exponent in (P4) is positive.

theorem HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity.sLower_pos {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : 0 < hP4.sLower

The lower regularity exponent in (P4) is positive.

theorem HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity.dim_div_xi_lt_sUpper {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : ↑d / ↑hP4.xi < hP4.sUpper

The P4 lower endpoint gives d / xi < sUpper.

theorem HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity.dim_div_xi_lt_sLower {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : ↑d / ↑hP4.xi < hP4.sLower

The P4 lower endpoint gives d / xi < sLower.

theorem HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity.upperMomentDenom_pos {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : 0 < ↑d / 2 + ↑d / ↑hP4.xi - hP4.sUpper

The upper geometric-series denominator in the Section 5.2 moment lemma is positive under (P4).

theorem HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity.lowerMomentDenom_pos {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : 0 < ↑d / 2 + ↑d / ↑hP4.xi - hP4.sLower

The lower geometric-series denominator in the Section 5.2 moment lemma is positive under (P4).

noncomputable def HCPolySupport.Book.Ch05.thetaAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (n : ℤ) : ℝ

The scalar contrast Theta_n = \bar\sigma_n \bar\sigma_{*,n}^{-1}, read from the Chapter 4 structural-law scalar surface.

Equations

• HCPolySupport.Book.Ch05.thetaAtScale hP hStruct n = hP.thetaAtScale hStruct n

@[simp]

theorem HCPolySupport.Book.Ch05.thetaAtScale_eq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (n : ℤ) : thetaAtScale hP hStruct n = hP.thetaAtScale hStruct n

noncomputable def HCPolySupport.Book.Ch05.widetildeThetaAtScale {d : ℕ} [NeZero d] (P : Ch04.RestrictionCoeffLaw d) (n : ℤ) (hP4 : QuantitativeCoarseGrainedEllipticity P) : ℝ

The high-moment contrast widetildeTheta_n with the parameters supplied by the Chapter 5 quantitative ellipticity input.

Equations

• HCPolySupport.Book.Ch05.widetildeThetaAtScale P n hP4 = HCPolySupport.Book.Ch04.widetildeThetaAtScale P n hP4.sUpper hP4.sLower hP4.xi

@[simp]

theorem HCPolySupport.Book.Ch05.widetildeThetaAtScale_eq {d : ℕ} [NeZero d] (P : Ch04.RestrictionCoeffLaw d) (n : ℤ) (hP4 : QuantitativeCoarseGrainedEllipticity P) : widetildeThetaAtScale P n hP4 = Ch04.widetildeThetaAtScale P n hP4.sUpper hP4.sLower hP4.xi

noncomputable def HCPolySupport.Book.Ch05.LambdaPositiveExcessMomentAtScale {d : ℕ} [NeZero d] (P : Ch04.RestrictionCoeffLaw d) (n : ℤ) (s : ℝ) (ξ : ℕ) (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) : ℝ

The positive excess of the upper ellipticity moment over the unit-scale structural-law scalar upper coefficient.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.Book.Ch05.LambdaPositiveExcessMomentAtScale_eq {d : ℕ} [NeZero d] (P : Ch04.RestrictionCoeffLaw d) (n : ℤ) (s : ℝ) (ξ : ℕ) (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) : LambdaPositiveExcessMomentAtScale P n s ξ hP hStruct = Ch04.annealedMomentRoot P ξ fun (a : RegCoeffField d) => max (Ch04.LambdaSqCoeffField (originCube d n) s (Ch02.MultiscaleExponent.finite 1) a - hP.barSigmaAtScale hStruct 0) 0

noncomputable def HCPolySupport.Book.Ch05.lambdaInvPositiveExcessMomentAtScale {d : ℕ} [NeZero d] (P : Ch04.RestrictionCoeffLaw d) (n : ℤ) (s : ℝ) (ξ : ℕ) (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) : ℝ

The positive excess of the lower inverse ellipticity moment over the unit-scale structural-law inverse-star coefficient.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.Book.Ch05.lambdaInvPositiveExcessMomentAtScale_eq {d : ℕ} [NeZero d] (P : Ch04.RestrictionCoeffLaw d) (n : ℤ) (s : ℝ) (ξ : ℕ) (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) : lambdaInvPositiveExcessMomentAtScale P n s ξ hP hStruct = Ch04.annealedMomentRoot P ξ fun (a : RegCoeffField d) => max ((Ch04.lambdaSqCoeffField (originCube d n) s (Ch02.MultiscaleExponent.finite 1) a)⁻¹ - (hP.barSigmaStarAtScale hStruct 0)⁻¹) 0

noncomputable def HCPolySupport.Book.Ch05.section52MomentBoundCoeff (d ξ : ℕ) (C s : ℝ) (m : ℕ) : ℝ

The displayed positive-excess coefficient in Section 5.2: C xi / (d / 2 + d / xi - s) * 3^{-(s - d / xi)m}.

Equations

• HCPolySupport.Book.Ch05.section52MomentBoundCoeff d ξ C s m = C * ↑ξ / (↑d / 2 + ↑d / ↑ξ - s) * Real.rpow 3 (-(s - ↑d / ↑ξ) * ↑m)

noncomputable def HCPolySupport.Book.Ch05.section52MomentLossCoeff (d ξ : ℕ) (s r : ℝ) : ℝ

The corrected two-exponent Section 5.2 moment-loss factor \Gamma_{s,r,\xi}. Here s is the unit-scale source exponent and r is the tracked exponent at scale m.

Equations

• HCPolySupport.Book.Ch05.section52MomentLossCoeff d ξ s r = s⁻¹ ^ 2 * (↑ξ / (↑d / 2 + ↑d / ↑ξ - r) + (r - s)⁻¹ ^ 2)

noncomputable def HCPolySupport.Book.Ch05.section52TwoExponentMomentBoundCoeff (d ξ : ℕ) (C s r : ℝ) (m : ℕ) : ℝ

The corrected two-exponent positive-excess coefficient in Section 5.2: C Gamma_{s,r,xi} * 3^{-(r - d / xi)m}.

Equations

• HCPolySupport.Book.Ch05.section52TwoExponentMomentBoundCoeff d ξ C s r m = C * HCPolySupport.Book.Ch05.section52MomentLossCoeff d ξ s r * Real.rpow 3 (-(r - ↑d / ↑ξ) * ↑m)

noncomputable def HCPolySupport.Book.Ch05.section52WidetildeThetaErrorCoeff (d ξ : ℕ) (C sMin : ℝ) (m : ℕ) : ℝ

The displayed widetildeTheta error coefficient in Section 5.2: C xi^2 3^{-(sMin - d / xi)m}.

Equations

• HCPolySupport.Book.Ch05.section52WidetildeThetaErrorCoeff d ξ C sMin m = C * ↑ξ ^ 2 * Real.rpow 3 (-(sMin - ↑d / ↑ξ) * ↑m)

noncomputable def HCPolySupport.Book.Ch05.section52WidetildeThetaCombinedCoeff (d ξ : ℕ) (CUpper CLower sUpper sLower : ℝ) : ℝ

The combined coefficient before the common Section 5.2 widetildeTheta scale.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch05.tauAtScale {d : ℕ} (P : Ch04.RestrictionCoeffLaw d) (n k : ℤ) (p q : Vec d) : ℝ

The annealed additivity defect tau_{n,k}(p,q) = E[J(cu_k,p,q)] - E[J(cu_n,p,q)].

Equations

• HCPolySupport.Book.Ch05.tauAtScale P n k p q = HCPolySupport.Book.Ch04.annealedResponseJAtScale P k p q - HCPolySupport.Book.Ch04.annealedResponseJAtScale P n p q

@[simp]

theorem HCPolySupport.Book.Ch05.tauAtScale_eq {d : ℕ} (P : Ch04.RestrictionCoeffLaw d) (n k : ℤ) (p q : Vec d) : tauAtScale P n k p q = Ch04.annealedResponseJAtScale P k p q - Ch04.annealedResponseJAtScale P n p q

noncomputable def HCPolySupport.Book.Ch05.sigmaHatAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) : ℝ

The scalar geometric mean \widehat\sigma_m = (\bar\sigma_m \bar\sigma_{*,m})^{1/2}.

Equations

• HCPolySupport.Book.Ch05.sigmaHatAtScale hP hStruct m = √(hP.barSigmaAtScale hStruct m * hP.barSigmaStarAtScale hStruct m)

@[simp]

theorem HCPolySupport.Book.Ch05.sigmaHatAtScale_eq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) : sigmaHatAtScale hP hStruct m = √(hP.barSigmaAtScale hStruct m * hP.barSigmaStarAtScale hStruct m)

noncomputable def HCPolySupport.Book.Ch05.specialPAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (e : Vec d) : Vec d

The special vector p_e = \widehat\sigma_m^{-1/2} e.

Equations

• HCPolySupport.Book.Ch05.specialPAtScale hP hStruct m e = (HCPolySupport.Book.Ch05.sigmaHatAtScale hP hStruct m).rpow (-(1 / 2)) • e

@[simp]

theorem HCPolySupport.Book.Ch05.specialPAtScale_eq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (e : Vec d) : specialPAtScale hP hStruct m e = (sigmaHatAtScale hP hStruct m).rpow (-(1 / 2)) • e

noncomputable def HCPolySupport.Book.Ch05.specialQAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (e : Vec d) : Vec d

The special vector q_e = \widehat\sigma_m^{1/2} e.

Equations

• HCPolySupport.Book.Ch05.specialQAtScale hP hStruct m e = (HCPolySupport.Book.Ch05.sigmaHatAtScale hP hStruct m).rpow (1 / 2) • e

@[simp]

theorem HCPolySupport.Book.Ch05.specialQAtScale_eq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (e : Vec d) : specialQAtScale hP hStruct m e = (sigmaHatAtScale hP hStruct m).rpow (1 / 2) • e

noncomputable def HCPolySupport.Book.Ch05.scalarizedResponseCenteringTerm {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (p q : Vec d) : ℝ

The scalar centering term 1/2 * (\bar\sigma_{*,m}^{-1} q - p) · (q - \bar\sigma_m p).

Equations

• HCPolySupport.Book.Ch05.scalarizedResponseCenteringTerm hP hStruct m p q = 1 / 2 * HCPolySupport.vecDot ((hP.barSigmaStarAtScale hStruct m)⁻¹ • q - p) (q - hP.barSigmaAtScale hStruct m • p)

@[simp]

theorem HCPolySupport.Book.Ch05.scalarizedResponseCenteringTerm_eq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (p q : Vec d) : scalarizedResponseCenteringTerm hP hStruct m p q = 1 / 2 * vecDot ((hP.barSigmaStarAtScale hStruct m)⁻¹ • q - p) (q - hP.barSigmaAtScale hStruct m • p)

noncomputable def HCPolySupport.Book.Ch05.expectedJScalarFormula {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (p q : Vec d) : ℝ

The scalarized expectation formula for the annealed response: 1/2 q · \bar\sigma_*^{-1} q - p · q + 1/2 p · \bar\sigma p.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.Book.Ch05.expectedJScalarFormula_eq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (p q : Vec d) : expectedJScalarFormula hP hStruct m p q = 1 / 2 * vecDot q ((hP.barSigmaStarAtScale hStruct m)⁻¹ • q) - vecDot p q + 1 / 2 * vecDot p (hP.barSigmaAtScale hStruct m • p)

noncomputable def HCPolySupport.Book.Ch05.tauScalarFormula {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (n k : ℤ) (p q : Vec d) : ℝ

The scalarized formula for tau_{n,k}(p,q) = E[J(cu_k,p,q)] - E[J(cu_n,p,q)].

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.Book.Ch05.tauScalarFormula_eq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (n k : ℤ) (p q : Vec d) : tauScalarFormula hP hStruct n k p q = 1 / 2 * vecDot p ((hP.barSigmaAtScale hStruct k - hP.barSigmaAtScale hStruct n) • p) + 1 / 2 * vecDot q (((hP.barSigmaStarAtScale hStruct k)⁻¹ - (hP.barSigmaStarAtScale hStruct n)⁻¹) • q)

noncomputable def HCPolySupport.Book.Ch05.centeredResponseExpectationFormula {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (p q : Vec d) : ℝ

The scalarized expectation of the centered response: 1/2 p · ((Theta_m - 1) q).

Equations

• HCPolySupport.Book.Ch05.centeredResponseExpectationFormula hP hStruct m p q = 1 / 2 * HCPolySupport.vecDot p ((HCPolySupport.Book.Ch05.thetaAtScale hP hStruct m - 1) • q)

@[simp]

theorem HCPolySupport.Book.Ch05.centeredResponseExpectationFormula_eq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (p q : Vec d) : centeredResponseExpectationFormula hP hStruct m p q = 1 / 2 * vecDot p ((thetaAtScale hP hStruct m - 1) • q)

noncomputable def HCPolySupport.Book.Ch05.restrictionCenteredResponseJObservableCubeSet {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (Q : TriadicCube d) (p q : Vec d) : RegCoeffField d → ℝ

The centered scalar response observable on a deterministic cube, with the centering scale supplied separately.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.Book.Ch05.restrictionCenteredResponseJObservableCubeSet_apply {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (Q : TriadicCube d) (p q : Vec d) (a : RegCoeffField d) : restrictionCenteredResponseJObservableCubeSet hP hStruct m Q p q a = Ch04.restrictionResponseJObservableCubeSet Q p q a - scalarizedResponseCenteringTerm hP hStruct m p q

noncomputable def HCPolySupport.Book.Ch05.restrictionCenteredResponseJStarObservableCubeSet {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (Q : TriadicCube d) (p q : Vec d) : RegCoeffField d → ℝ

The centered adjoint scalar response observable on a deterministic cube.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.Book.Ch05.restrictionCenteredResponseJStarObservableCubeSet_apply {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (Q : TriadicCube d) (p q : Vec d) (a : RegCoeffField d) : restrictionCenteredResponseJStarObservableCubeSet hP hStruct m Q p q a = Ch04.restrictionResponseJObservableCubeSet Q p q (adjointReg a) - scalarizedResponseCenteringTerm hP hStruct m p q

noncomputable def HCPolySupport.Book.Ch05.expectedCenteredResponseJAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (p q : Vec d) : ℝ

The expected centered scalar response on the origin cube at scale m.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch05.expectedCenteredResponseJStarAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (p q : Vec d) : ℝ

The expected centered adjoint scalar response on the origin cube at scale m.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch05.annealedConvergenceEntryScaleBound {d : ℕ} [NeZero d] (P : Ch04.RestrictionCoeffLaw d) (hP4 : QuantitativeCoarseGrainedEllipticity P) (C : ℝ) : ℕ

The first ceiling contribution in the annealed entry scale, depending on the unit-scale value of widetildeTheta.

Equations

• HCPolySupport.Book.Ch05.annealedConvergenceEntryScaleBound P hP4 C = ⌈C * Real.log (2 + HCPolySupport.Book.Ch05.widetildeThetaAtScale P 0 hP4) ^ 2⌉₊

noncomputable def HCPolySupport.Book.Ch05.annealedConvergenceSigmaTailScale {d : ℕ} [NeZero d] (P : Ch04.RestrictionCoeffLaw d) (hP4 : QuantitativeCoarseGrainedEllipticity P) (C sigma : ℝ) : ℕ

The second ceiling contribution in the annealed entry scale, depending on the target perturbative accuracy sigma.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch05.annealedEntryScale {d : ℕ} [NeZero d] (P : Ch04.RestrictionCoeffLaw d) (hP4 : QuantitativeCoarseGrainedEllipticity P) (C sigma : ℝ) : ℕ

The entry scale N_sigma from the main annealed convergence theorem.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch05.annealedAlgebraicEntryScale {d : ℕ} [NeZero d] (P : Ch04.RestrictionCoeffLaw d) (hP4 : QuantitativeCoarseGrainedEllipticity P) (C : ℝ) : ℕ

The algebraic-decay entry scale N_0 in Theorem t.annealed.convergence.

This is the two-ceiling scale used after the perturbative entry scale has been dilated to unit scale and the small-contrast algebraic iteration has been applied.

Equations

• One or more equations did not get rendered due to their size.