LoadNormalization

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

Load normalization for the unconditional response estimate

The unconditional response estimate is proved at the loading ((mu sigma0)^{-1/2} e, (mu sigma0)^{1/2} e). The source first removes the mu-part of the loading with e.shaking.lambda

applied with lam = mu, p = sigma0^{-1/2} e and q = sigma0^{1/2} e, and then applies the conditional response estimate cube-by-cube at the mesoscopic scale.

This module contains the load-normalization algebra of that step, together with the mesoscale factor bookkeeping of the four frozen terms of responseJ_sensitivity_unconditional. Everything here is proved.

What is here

• le_of_shaking_lambda_bound — the gauge-free arithmetic that turns the square on the right of e.shaking.lambda into the two frozen terms 2 mu^{-1} J and mu^{-1} (mu - 1)^2 V.

Consumption points (deliberately NOT proved here)

1. e.shaking.lambda. There is no Lean declaration for it in CoarseGraining or in this repository (only the exact scaling identity responseJ_homogeneous). le_of_shaking_lambda_bound is written so that the shaking-lambda inequality enters as a hypothesis of the caller, not of any statement of this module.
2. The conditional response estimate at mesoscopic cubes (frozen theorem responseJ_sensitivity at delta = 1), stated on descendant cubes.

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

The mu-normalization arithmetic

theorem Algsuperdiff.Section24.Sensitivity.Provider.Mesoscale.le_of_shaking_lambda_bound {K J V μ : ℝ} (hμ : 0 < μ) (hJ : 0 ≤ J) (hV : 0 ≤ V) (hK : K ≤ μ⁻¹ * (√J + √2⁻¹ * |μ - 1| * √V) ^ 2) : K ≤ 2 * μ⁻¹ * J + μ⁻¹ * (μ - 1) ^ 2 * V

The mu-normalization arithmetic of e.shaking.lambda. Any quantity bounded by the right-hand side of the shaking-lambda inequality at lam = mu is bounded by the two frozen terms 2 mu^{-1} J and mu^{-1} (mu - 1)^2 V.

The shaking-lambda inequality itself is a consumption point: it enters as the hypothesis hK supplied by the caller.