GammaTenGaugeScalarCap #

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

The two scalar gauge factors of the Besov legs are capped #

ABK26, e.shom.h.bounds, read at Step 2 of l.approximate.recurrence.formula, e.Fz.def.

The gap this module fills #

cubeBesovPositiveVectorPartialSeminormTwo_gauged_localizationFz_potential and ..._flux identify the Besov tower of each gauged leg of bfF_z with a scalar multiple of the tower of the raw field, the two scalars being

  c_1 = sqrt(sigma_0) . sqrt(shom_n)^{-1} ,   c_2 = sqrt(sigma_0)^{-1} . sqrt(shom_n) ,

at sigma_0 = shom_{n+h-1}. Closure.GammaTenStripEnvelopeTwoLeg carries |c_1| <= C_g and |c_2| <= C_g as binders and no producer exists. The proved PrincipalResponseComposeDisplayTwo.gaugeRatio_sigmaBar_le_readingConst caps the ratio max(shom_{n+h-1}/shom_n, shom_n/shom_{n+h-1}) by the absolute 4 . 3^9; each |c_i| is the square root of one of those two quotients, and a square root of a number above 1 is below the number itself. That is the whole content.

What is proved #

sqrt_le_self_of_one_le --- sqrt C <= C for 1 <= C.
abs_sqrt_mul_inv_sqrt_le --- |sqrt a . (sqrt b)^{-1}| <= C from a / b <= C and 1 <= C, for positive a, b.
abs_gaugeScalar_potential_le, abs_gaugeScalar_flux_le --- the two caps at the closure's own pair of gauges, from the proved ratio cap carried as the binder hgauge.

Binders #

Only hgauge, the same binder Closure.GammaTenCloserGauge.blockVecNormSum_blockGaugeUp_le_gammaTenGaugeConst already carries and which Closure.ClosureInteriorSplit discharges inline from PrincipalResponseComposeDisplayTwo.gaugeRatio_sigmaBar_le_readingConst. No smallness gate, no moment, no measurability and no sample-space proposition occurs.

Scope #

Internal Provider infrastructure for the Step-2 fluctuation estimate. There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.