PerCubeFluctuationArithmetic

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

Provider: the per-cube fluctuation arithmetic of Step 2

Source displays in ABK26, inside Step 2 of l.approximate.recurrence.formula:

• The Euler--Lagrange identity followed by the block Besov duality bound

  fint tilde S_z . bfA_m tilde S_z
    = fint bfF_z . bfA_m tilde S_z
    <= [bfAhom^{1/2} bfF_z]_{H^1} [bfAhom^{-1/2} bfA_m tilde S_z]_{H^{-1}};
  

• The doubled coarse-grained Poincare inequality e.CG.Poincare.doubled.vars, which bounds the H^{-1} factor linearly in || bfA_m^{1/2} tilde S_z ||;

• The resulting bound on || bfA_m^{1/2} tilde S_z || itself, obtained by cancelling one power, and the companion cross-term bound for P_z. fint bfA_m tilde S_z;

• The display e.lower.bound.localization.terms, whose bracketed integrand is 2 P_z. fint bfA_m tilde S_z + fint tilde S_z. bfA_m tilde S_z.

Scope: arithmetic only

Everything below is abstract real arithmetic over bare real variables. No cube, no seminorm, no coefficient field, no minimizer and no gauge occurs, and this module imports nothing but Mathlib.Analysis.SpecialFunctions.Pow.Real. The three analytic inputs of the displays above --- the block Besov duality bound, the doubled coarse-grained Poincare inequality, and the Euler--Lagrange identity that supplies the quadratic value --- appear here only as the named real hypotheses hquad, hpoin, hquadval and hcross. Each is a caller obligation, to be discharged by the caller at whatever carrier it works on; this module neither states nor proves any of them. Isolating the algebra here keeps every numeric tactic away from Real.rpow terms.

Under the intended instantiation blockE = || bfA_m^{1/2} tilde S_z ||, E = fint tilde S_z . bfA_m tilde S_z / 2, Bu = [bfAhom^{-1/2} bfA_m tilde S_z]_{H^{-1}}, Bg = [bfAhom^{1/2} bfF_z]_{H^1}, normP = | bfAhom^{1/2} P_z |, kappa the block Besov duality constant and Theta the doubled-Poincare ellipticity factor.

theorem Algsuperdiff.Section3.Provider.Variational.le_of_mul_self_le_mul_of_nonneg {t A : ℝ} (ht : 0 ≤ t) (hA : 0 ≤ A) (h : t * t ≤ A * t) : t ≤ A

Self-improvement. A nonnegative quantity whose square is dominated by a nonnegative multiple of itself is dominated by that multiple. This is the step that turns a quadratic bound plus a linear Poincare bound into a bound on the quantity itself.

theorem Algsuperdiff.Section3.Provider.Variational.blockEnergyNorm_le_of_poincare_bound {E blockE Bu Bg kappa Theta : ℝ} (hblockE : 0 ≤ blockE) (hsq : blockE * blockE = 2 * E) (hkappa : 0 ≤ kappa) (hBg : 0 ≤ Bg) (hTheta : 0 ≤ Theta) (hquad : 2 * E ≤ kappa * (Bu * Bg)) (hpoin : Bu ≤ Theta * blockE) : blockE ≤ kappa * Theta * Bg

The self-improved bound on || bfA_m^{1/2} tilde S_z ||, over abstract reals. If the doubled energy E satisfies the duality bound 2E ≤ kappa (Bu Bg), the Poincare bound Bu ≤ Theta blockE holds, and blockE² = 2E, then blockE ≤ kappa Theta Bg.

Conditional helper A: hsq, hquad and hpoin are caller obligations.

theorem Algsuperdiff.Section3.Provider.Variational.perCube_fluct_le {cross quad E blockE Bu Bg kappa Theta normP : ℝ} (hnormP : 0 ≤ normP) (hkappa : 0 ≤ kappa) (hBg : 0 ≤ Bg) (hTheta : 0 ≤ Theta) (hblockE : 0 ≤ blockE) (hsq : blockE * blockE = 2 * E) (hcross : cross ≤ normP * Bu) (hquad : 2 * E ≤ kappa * (Bu * Bg)) (hpoin : Bu ≤ Theta * blockE) (hquadval : quad = 2 * E) : 2 * cross + quad ≤ 2 * (kappa * Theta * Theta) * normP * Bg + kappa * Theta * Bg * (kappa * Theta * Bg)

The bracketed integrand, per cube, over abstract reals. Combining the cross-term bound, the duality bound coming from the Euler--Lagrange identity and the Poincare self-improvement:

2 P_z . fint bfA_m tilde S_z + fint tilde S_z . bfA_m tilde S_z
  <= 2 kappa Theta² normP Bg + (kappa Theta Bg)² .

Both summands carry exactly the manuscript's power of the ellipticity factor: once in the cross term and once in the quadratic term.

Conditional helper A: hsq, hcross, hquad, hpoin and hquadval are caller obligations, to be discharged at the caller's carrier.