LambdaShaking

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

The shaking-lambda source estimate e.shaking.lambda

This module proves the source estimate e.shaking.lambda: for every bounded Lipschitz domain U, every coefficient field a, every p, q and every lambda > 0,

This is the missing input of Mesoscale.LoadNormalization, whose le_of_shaking_lambda_bound consumes exactly the right-hand side above with lam = mu.

Route

The source proof combines e.homogeneity.in.a + e.homogeneous.J (scaling the coefficient field), e.J.magic.squares (the completed-square rearrangement of J in terms of sigma, sigma_*, k), e.ksym.by.sss (nonnegativity of the p-only part of the magic-squares formula) and Young's inequality with a free parameter eps, optimized at the end.

Neither e.homogeneity.in.a nor the literal magic-squares identity is available as a Lean statement at the Domain/CoeffOn level of the frozen sensitivity anchors: CoarseGraining's coefficient-field homogeneity lives on the Set-based CoarseGraining.ResponseJ layer (responseJ_homogeneous_coeffField), and there is no Book.Ch02 declaration for e.J.magic.squares. Both are replaced here by an equivalent and strictly cheaper route through the unconditional Chapter 2 coarse-matrix formula responseJ_eq_coarseMatrices_formula_canonical:

• responseJ_smul (quadraticity, unconditional) replaces e.homogeneity.in.a and e.homogeneous.J: it gives the exact identity J(U, lam^{-1/2} p, lam^{1/2} q) = lam^{-1} J(U, p, lam q).
• The coarse-matrix formula gives the quadratic expansion in the q-slot (responseJ_smul_right_eq below): J(U,p,t q) = J(U,0,q) t^2 + (J(U,p,q) - J(U,p,0) - J(U,0,q)) t + J(U,p,0). This is e.J.magic.squares in coordinates: the magic-squares formula says exactly that this quadratic is a nonnegative constant plus a sigma_*^{-1}-square, i.e. that its discriminant is nonpositive.
• responseJ_nonneg (unconditional) applied along the whole line t gives the discriminant inequality sq_mixed_le. This replaces e.ksym.by.sss: the source uses e.ksym.by.sss only to know that the p-only part of the magic-squares formula is nonnegative, which is the same statement as nonnegativity of J at the minimizing q.
• The discriminant inequality is exactly what Young + optimization in eps produce, so the closed (optimized) form is obtained directly and the eps-form is recovered from it by Young's inequality.

Nothing in this module is conditional: every hypothesis is a source binder (0 < lam, and 0 < eps for the pre-optimization form).

What is here

• responseJ_smul_right_eq, sq_mixed_le, responseJ_smul_right_le — private helpers (the quadratic expansion, its discriminant, and the resulting one-parameter estimate).
• responseJ_shaking_lambda — the source estimate at a general domain, in the exact shape consumed by Mesoscale.LoadNormalization.le_of_shaking_lambda_bound.
• responseJ_shaking_lambda_epsilon — the pre-optimization eps-form.
• responseJ_shaking_lambda_normalizedLoading, responseJ_shaking_lambda_normalizedLoading_epsilon — the same two estimates read at the frozen loading ((mu sigma0)^{-1/2} e, (mu sigma0)^{1/2} e).

Every declaration in this module is an internal helper for the Section 2.4 sensitivity providers.

The quadratic expansion of J in the flux slot

The one-parameter estimate

The source estimate

theorem Algsuperdiff.Section24.Sensitivity.Provider.Shaking.responseJ_shaking_lambda {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (p q : HCPolySupport.Vec d) {lam : ℝ} (hlam : 0 < lam) : HCPolySupport.Book.Ch02.responseJ U a ((√lam)⁻¹ • p) (√lam • q) ≤ lam⁻¹ * (√(HCPolySupport.Book.Ch02.responseJ U a p q) + √2⁻¹ * |lam - 1| * √(HCPolySupport.vecDot q (HCPolySupport.matVecMul (HCPolySupport.Book.Ch02.sigmaStarInvCoarse U a) q))) ^ 2

e.shaking.lambda at a general bounded Lipschitz domain: for every p, q and every lam > 0,

The right-hand side is written in exactly the shape consumed by the hypothesis hK of Mesoscale.LoadNormalization.le_of_shaking_lambda_bound.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Shaking.responseJ_shaking_lambda_epsilon {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (p q : HCPolySupport.Vec d) {lam eps : ℝ} (hlam : 0 < lam) (heps : 0 < eps) : HCPolySupport.Book.Ch02.responseJ U a ((√lam)⁻¹ • p) (√lam • q) ≤ (1 + eps) / lam * HCPolySupport.Book.Ch02.responseJ U a p q + (1 + eps) / (2 * eps * lam) * (lam - 1) ^ 2 * HCPolySupport.vecDot q (HCPolySupport.matVecMul (HCPolySupport.Book.Ch02.sigmaStarInvCoarse U a) q)

The pre-optimization (eps) form of e.shaking.lambda: for every `eps

0, J(U, lam^{-1/2} p, lam^{1/2} q; a) <= (1+eps)/lam J(U,p,q;a) + (1+eps)/(2 eps lam) (lam-1)^2 (q. sigma_*^{-1}(U;a) q)`.

The closed form responseJ_shaking_lambda is the optimization of this bound in eps; it is proved first here and this display is recovered from it by Young's inequality, so the two are equivalent.

The frozen loading

theorem Algsuperdiff.Section24.Sensitivity.Provider.Shaking.responseJ_shaking_lambda_normalizedLoading {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) {mu sigma0 : ℝ} (hmu : 0 < mu) (e : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.responseJ U a ((√(mu * sigma0))⁻¹ • e) (√(mu * sigma0) • e) ≤ mu⁻¹ * (√(HCPolySupport.Book.Ch02.responseJ U a ((√sigma0)⁻¹ • e) (√sigma0 • e)) + √2⁻¹ * |mu - 1| * √(HCPolySupport.vecDot (√sigma0 • e) (HCPolySupport.matVecMul (HCPolySupport.Book.Ch02.sigmaStarInvCoarse U a) (√sigma0 • e)))) ^ 2

e.shaking.lambda at the frozen loading. Reading responseJ_shaking_lambda with lam = mu, p = sigma0^{-1/2} e and q = sigma0^{1/2} e, the left-hand side is literally the loading ((mu sigma0)^{-1/2} e, (mu sigma0)^{1/2} e) of responseJ_sensitivity_unconditional, and the right-hand side is exactly the hypothesis hK of Mesoscale.LoadNormalization.le_of_shaking_lambda_bound at K = J(U, (mu sigma0)^{-1/2} e, (mu sigma0)^{1/2} e), J = J(U, sigma0^{-1/2} e, sigma0^{1/2} e) and V = (sigma0^{1/2} e) . sigma_*^{-1}(U;a) (sigma0^{1/2} e).

theorem Algsuperdiff.Section24.Sensitivity.Provider.Shaking.responseJ_shaking_lambda_normalizedLoading_epsilon {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) {mu sigma0 eps : ℝ} (hmu : 0 < mu) (heps : 0 < eps) (e : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.responseJ U a ((√(mu * sigma0))⁻¹ • e) (√(mu * sigma0) • e) ≤ (1 + eps) / mu * HCPolySupport.Book.Ch02.responseJ U a ((√sigma0)⁻¹ • e) (√sigma0 • e) + (1 + eps) / (2 * eps * mu) * (mu - 1) ^ 2 * HCPolySupport.vecDot (√sigma0 • e) (HCPolySupport.matVecMul (HCPolySupport.Book.Ch02.sigmaStarInvCoarse U a) (√sigma0 • e))

The eps-form of e.shaking.lambda at the frozen loading.