StepSevenLambdaStability

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

t.regularity Step 7b, clause (A): l.lambdas.stability at s* = 1/16

The target

ABK26 l.lambdas.stability (statement, proof):

  There is C(d) < ∞ such that for every p, q ∈ [1,∞], s, t ∈ (0,1/2] with s < t,
  and x ∈ □_0 with x + □_{-1} ⊆ □_0,
      λ_{t,q}^{-1}(x+□_{-1}; a) ≤ C(1-2s)^{-1}(t/(t-s))^{2/q} λ_{s,q}^{-1}(□_0; a) ,
      Λ_{t,q}(x+□_{-1}; a)      ≤ C(1-2s)^{-1}(t/(t-s))^{2/q} Λ_{s,q}(□_0; a) .

That is what is delivered here, at the printed prefactor shape C/(1-2s*)·(t/(t-s*))^{2/q} with the explicit constant C = 2.

Carrier scope: what is delivered, and the one restriction

Ch02.lambdaSq/Ch02.LambdaSq are functions of a TriadicCube d, which is a scale : ℤ together with an integer index : Fin d → ℤ. A cube y + □_{k-1} with y off the scale-(k-1) lattice is therefore not an object of the carrier at all: the printed lemma's hypothesis "x ∈ □_0 with x + □_{-1} ⊆ □_0" ranges over arbitrary real x, and for non-lattice x the term λ_{t,q}(x+□_{-1}; a) does not type.

What is expressible, and what this module proves, is the printed inequality for the lattice-aligned configuration: the inner cube is a triadic descendant of the outer one. That is exactly the printed configuration when the Step-7a sandwich centre can be taken to be the window centre itself (y' = z, i.e. when z + □_{k'-1} ⊆ □_m, so the clamp is the identity), and the outer/inner pair is (z + □_{k'}, z + □_{k'-1}) — a parent and its centre child. Everything downstream in §4.4 runs on originCube d k with the translation absorbed into the coefficient family and the solution's argument (see StepSevenMean.exists_stepSevenEnd_chain_of_lambda_hmeanFree), so this is the configuration the proved chain consumes.

The proof, and what CoarseGraining supplied

The printed proof builds a Whitney-type family and sums a geometric series. In the lattice-aligned configuration none of that is needed: CoarseGraining already proves the two halves separately and the lemma is their composition.

• index monotonicity on ONE cube — Ch02.lambdaSq_mono, Ch02.LambdaSq_antitone (ABK26 e.ellipticities.monotone.ordered): λ_{s,q}^{-1} and Λ_{s,q} are nonincreasing in the index, so passing from t down to s* costs nothing;
• one-scale descent at a fixed index — Ch02.descendant_lambdaSq_inv_le, Ch02.descendant_LambdaSq_le (ABK26 e.bound.one.cube.by.lambdas): a descendant at scale k costs 3^{2s(m-k)}, here 3^{2s*}.

So the honest constant of the composition is 3^{2s*} = 3^{1/8} ≤ 2, and the printed prefactor — whose smallest possible value at s* = 1/16 is C·8/7 ≥ 8/7 — dominates it at C = 2. The printed C(d) is realized dimension-free here; that is a strengthening, not a weakening.

Strengthenings (binders dropped)

• the printed range binder t ≤ 1/2 is NOT taken: the estimate is proved for every t > s*;
• the printed p ∈ [1,∞] binder is absent because the p of the printed lemma belongs only to its third display (the 𝓔 twin), which is not built here;
• the constant is dimension-free.

What is NOT built here

The 𝓔 twin e.mathcalE.stability. §4.4's Step 7b applies only the λ and Λ displays (e.lambda.stability.applied).

References

• ABK26, l.lambdas.stability; e.lambda.stability.applied; e.ellipticities.monotone.ordered; e.bound.one.cube.by.lambdas.

1. The re-specified stability index and the printed prefactor

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepSevenStabilityIndex : ℝ

The fixed exponent used for the seventh-step stability comparison.

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepSevenStabilityIndex = 1 / 16

@[simp]

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenStabilityIndex_eq : stepSevenStabilityIndex = 1 / 16

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenStabilityIndex_pos : 0 < stepSevenStabilityIndex

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepSevenStabilityConst : ℝ

The fixed multiplicative constant used for the seventh-step stability comparison.

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepSevenStabilityConst = 2

@[simp]

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenStabilityConst_eq : stepSevenStabilityConst = 2

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepSevenStabilityExponentFactor (s t : ℝ) : HCPolySupport.Book.Ch02.MultiscaleExponent → ℝ

The printed exponent factor (t/(t-s))^{2/q}, with the q = ∞ endpoint value 1 (the limit of the finite-q expression).

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepSevenStabilityExponentFactor s t (HCPolySupport.Book.Ch02.MultiscaleExponent.finite q) = (t / (t - s)).rpow (2 / q)
• Algsuperdiff.Section4.Provider.Regularity.stepSevenStabilityExponentFactor s t HCPolySupport.Book.Ch02.MultiscaleExponent.infinity = 1

@[simp]

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenStabilityExponentFactor_finite (s t q : ℝ) : stepSevenStabilityExponentFactor s t (HCPolySupport.Book.Ch02.MultiscaleExponent.finite q) = (t / (t - s)).rpow (2 / q)

@[simp]

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenStabilityExponentFactor_infinity (s t : ℝ) : stepSevenStabilityExponentFactor s t HCPolySupport.Book.Ch02.MultiscaleExponent.infinity = 1

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepSevenStabilityPrefactor (C s t : ℝ) (q : HCPolySupport.Book.Ch02.MultiscaleExponent) : ℝ

The stability prefactor including the scale-gap exponent factor.

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepSevenStabilityPrefactor C s t q = C / (1 - 2 * s) * Algsuperdiff.Section4.Provider.Regularity.stepSevenStabilityExponentFactor s t q

theorem Algsuperdiff.Section4.Provider.Regularity.one_le_stepSevenStabilityExponentFactor {s t : ℝ} (hs : 0 < s) (hst : s < t) {q : HCPolySupport.Book.Ch02.MultiscaleExponent} (hq : q.IsAdmissible) : 1 ≤ stepSevenStabilityExponentFactor s t q

The exponent factor is at least 1: t/(t-s) ≥ 1 and 2/q ≥ 0.

theorem Algsuperdiff.Section4.Provider.Regularity.rpow_three_two_mul_stabilityIndex_le_two : Real.rpow 3 (2 * stepSevenStabilityIndex) ≤ 2

3^{2s*} = 3^{1/8} ≤ 2: the honest constant of the lattice-aligned composition.

theorem Algsuperdiff.Section4.Provider.Regularity.rpow_three_le_stepSevenStabilityPrefactor {t : ℝ} {q : HCPolySupport.Book.Ch02.MultiscaleExponent} (hst : stepSevenStabilityIndex < t) (hq : q.IsAdmissible) : Real.rpow 3 (2 * stepSevenStabilityIndex) ≤ stepSevenStabilityPrefactor stepSevenStabilityConst stepSevenStabilityIndex t q

The honest constant is dominated by the printed prefactor at s* = 1/16 and C = 2: 3^{1/8} ≤ 2 ≤ (16/7)·(t/(t-s*))^{2/q}.

2. The two CoarseGraining halves

theorem Algsuperdiff.Section4.Provider.Regularity.lambdaSq_inv_le_of_index_le {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) {s t : ℝ} {q : HCPolySupport.Book.Ch02.MultiscaleExponent} (hs : 0 < s) (hst : s < t) (hq : q.IsAdmissible) : (HCPolySupport.Book.Ch02.lambdaSq Q t q a)⁻¹ ≤ (HCPolySupport.Book.Ch02.lambdaSq Q s q a)⁻¹

Index monotonicity of λ^{-1} on one cube (e.ellipticities.monotone.ordered): λ_{s,q}^{-1} is nonincreasing in the index.

theorem Algsuperdiff.Section4.Provider.Regularity.multiscaleDescendantWeight_pred {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) : HCPolySupport.Book.Ch02.multiscaleDescendantWeight Q (Q.scale - 1) s = Real.rpow 3 (2 * s)

The one-scale descent weight at depth one: multiscaleDescendantWeight Q (Q.scale - 1) s = 3^{2s}.

3. Clause (A), general depth

theorem Algsuperdiff.Section4.Provider.Regularity.lambdaSq_inv_stability_of_descendant {d : ℕ} [NeZero d] {Q R : HCPolySupport.TriadicCube d} {k : ℤ} (a : HCPolySupport.Book.Ch03.CoeffFamily d) {s t : ℝ} {q : HCPolySupport.Book.Ch02.MultiscaleExponent} (hR : R ∈ HCPolySupport.descendantsAtScale Q k) (hs : 0 < s) (hst : s < t) (hq : q.IsAdmissible) : (HCPolySupport.Book.Ch02.lambdaSq R t q a)⁻¹ ≤ HCPolySupport.Book.Ch02.multiscaleDescendantWeight Q k s * (HCPolySupport.Book.Ch02.lambdaSq Q s q a)⁻¹

Clause (A), lower constant, at a general descendant scale. For every descendant R of Q at scale k and every index pair s < t,

  λ_{t,q}^{-1}(R; a) ≤ 3^{2s(Q.scale-k)} · λ_{s,q}^{-1}(Q; a) .

theorem Algsuperdiff.Section4.Provider.Regularity.LambdaSq_stability_of_descendant {d : ℕ} [NeZero d] {Q R : HCPolySupport.TriadicCube d} {k : ℤ} (a : HCPolySupport.Book.Ch03.CoeffFamily d) {s t : ℝ} {q : HCPolySupport.Book.Ch02.MultiscaleExponent} (hR : R ∈ HCPolySupport.descendantsAtScale Q k) (hs : 0 < s) (hst : s < t) (hq : q.IsAdmissible) : HCPolySupport.Book.Ch02.LambdaSq R t q a ≤ HCPolySupport.Book.Ch02.multiscaleDescendantWeight Q k s * HCPolySupport.Book.Ch02.LambdaSq Q s q a

Clause (A), upper constant, at a general descendant scale.

  Λ_{t,q}(R; a) ≤ 3^{2s(Q.scale-k)} · Λ_{s,q}(Q; a) .

4. Clause (A) in the printed shape, at s* = 1/16

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenLambdaStability_lambdaInv {d : ℕ} [NeZero d] {Q R : HCPolySupport.TriadicCube d} (a : HCPolySupport.Book.Ch03.CoeffFamily d) {t : ℝ} {q : HCPolySupport.Book.Ch02.MultiscaleExponent} (hR : R ∈ HCPolySupport.descendantsAtScale Q (Q.scale - 1)) (hst : stepSevenStabilityIndex < t) (hq : q.IsAdmissible) : (HCPolySupport.Book.Ch02.lambdaSq R t q a)⁻¹ ≤ stepSevenStabilityPrefactor stepSevenStabilityConst stepSevenStabilityIndex t q * (HCPolySupport.Book.Ch02.lambdaSq Q stepSevenStabilityIndex q a)⁻¹

Clause (A), the printed lower display e.lambda.stability at the re-specified index, in the lattice-aligned configuration: for every triadic cube Q, every centre child / one-scale descendant R, every t > s* and every admissible q ∈ [1,∞],

  λ_{t,q}^{-1}(R; a)
    ≤ C(1-2s*)^{-1}(t/(t-s*))^{2/q} λ_{s*,q}^{-1}(Q; a) ,      C = 2 .

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenLambdaStability_Lambda {d : ℕ} [NeZero d] {Q R : HCPolySupport.TriadicCube d} (a : HCPolySupport.Book.Ch03.CoeffFamily d) {t : ℝ} {q : HCPolySupport.Book.Ch02.MultiscaleExponent} (hR : R ∈ HCPolySupport.descendantsAtScale Q (Q.scale - 1)) (hst : stepSevenStabilityIndex < t) (hq : q.IsAdmissible) : HCPolySupport.Book.Ch02.LambdaSq R t q a ≤ stepSevenStabilityPrefactor stepSevenStabilityConst stepSevenStabilityIndex t q * HCPolySupport.Book.Ch02.LambdaSq Q stepSevenStabilityIndex q a

Clause (A), the printed upper display e.big.Lambda.stability at the re-specified index, in the lattice-aligned configuration:

  Λ_{t,q}(R; a) ≤ C(1-2s*)^{-1}(t/(t-s*))^{2/q} Λ_{s*,q}(Q; a) ,      C = 2 .

5. The lattice-aligned Step-7a sandwich pair

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenCentreChild_mem_descendantsAtScale (d : ℕ) (k : ℤ) : HCPolySupport.originCube d (k - 1) ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d k) (k - 1)

The centre child □_{k-1} ⊆ □_k: the lattice-aligned instance of the Step-7a sandwich, in which the clamp of StepSevenSandwich.exists_sandwich_centre is the identity (y' = z) and the translation is absorbed into the coefficient family.

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenLambdaStability_centreChild {d : ℕ} [NeZero d] (k : ℤ) (a : HCPolySupport.Book.Ch03.CoeffFamily d) {t : ℝ} {q : HCPolySupport.Book.Ch02.MultiscaleExponent} (hst : stepSevenStabilityIndex < t) (hq : q.IsAdmissible) : (HCPolySupport.Book.Ch02.lambdaSq (HCPolySupport.originCube d (k - 1)) t q a)⁻¹ ≤ stepSevenStabilityPrefactor stepSevenStabilityConst stepSevenStabilityIndex t q * (HCPolySupport.Book.Ch02.lambdaSq (HCPolySupport.originCube d k) stepSevenStabilityIndex q a)⁻¹ ∧ HCPolySupport.Book.Ch02.LambdaSq (HCPolySupport.originCube d (k - 1)) t q a ≤ stepSevenStabilityPrefactor stepSevenStabilityConst stepSevenStabilityIndex t q * HCPolySupport.Book.Ch02.LambdaSq (HCPolySupport.originCube d k) stepSevenStabilityIndex q a

Clause (A) at the Step-7a sandwich pair (□_{k-1}, □_k), both displays, in the printed indexing (k'-1, k').