GoodLocalEvents #

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

The good local sensitivity event `e.good.local.events` #

ABK26 defines, in e.good.local.events, for m, n integers and a centre z, the event

Q(m,n,z) := { C_sens sup_{L >= n} 3^{2m} ||grad (k_L - k_n)||_{W^{1,infinity}(z+square_m)}
              <= (1/2) C_{(e.cg.ellip.lower)}^{-1} 3^{-(1/2)(n-m)_+} sigmaBar_{n-1}
              <= 3^{-(1/4)(n-m)_+} lambda_{1/8,2}(z+square_m; a_n) } ,

a chain of two inequalities around the common middle threshold goodLocalThreshold M Ccg m n. Its stated purpose is that it "allows us to switch from the field a_L to a_n in the cube z+square_m for any L >= n, using the coarse-grained sensitivity estimates".

This module assembles the event from its two proved clauses and proves that switch, i.e. that on the event the rescaled literal increment k_L - k_n meets the smallness gate of the frozen Section 2.4 sensitivity lemmas.

the sensitivity clause goodLocalSensitivity is the first inequality, measured by the two-index gauge incrementOscGauge₂ of IncrementGaugeTwoIndex;
the coarse-ellipticity clause is the proved goodLocalEllipticity of GoodLocalEllipticity;
goodLocalEvent is their intersection, which is the displayed chain.

Reading conventions (recorded; none of them is a manuscript defect) #

The supremum. The manuscript's sup_{L >= n} ... <= T is denoted by the equivalent universally quantified form forall L >= n, ... <= T: a supremum is below T exactly when every member of the family is. Membership in the event unfolds to exactly that quantified form (mem_goodLocalSensitivity_iff), and the event is correspondingly the intersection over L >= n of the one-index gates (goodLocalSensitivity_eq_iInter). The iSup of an unbounded real family is a junk value, so the universally quantified form is the faithful denotation, not a weakening.
The centre. z is carried by a TriadicCube d: m = Q.scale and cubeSet Q = z + square_m with z in 3^m Z^d. The manuscript writes z in R^d; every consumer of e.good.local.events instantiates z in a triadic lattice, and this repository has no multiscale ellipticity observable on off-grid translates.
The two constants. C_{(e.cg.ellip.lower)} is the explicit real parameter Ccg of GoodLocalEllipticity (the now-proved frozen coarse_ellipticity_bounds supplies it to downstream consumers, while this conditional A remains parametrized). The joint smallness constant C_{(e.J.sensitivity.smallness.condition)&(e.lambda.sensitivity.smallness.condition)} is sensitivityConstMax d of DeltaOsc, the single dimension-only constant that dominates both frozen sensitivity constants.
No positivity of Ccg is used by the gate opening: the chain C_sens * gauge <= threshold <= 3^{-(1/4)(n-m)_+} lambda passes through the threshold without inspecting it.

The remaining input: the lambda-transfer #

The frozen Section 2.4 gates are stated at the unit cube, against unitCubeLambda (3/8) (.finite 2) a; the event is stated at z + square_m, against lambda_{1/8,2}(z+square_m; a_n). Bridging the two needs

lambda_{1/8,2}(z+square_m; a_n)  <=  lambda_{3/8,2}(unit cube; a_rescaled) ,

which is the composition of

the exponent monotonicity e.ellipticities.monotone.ordered (ABK26): lambda_{t,q} <= lambda_{s,q} for 0 < t < s, here at t = 1/8 < 3/8 = s; and
the scale-and-translation covariance of the multiscale lower ellipticity, lambda_{s,q}(z + square_m; a) = unitCubeLambda s q (a rescaled by y |-> z
- 3^m y). CoarseGraining has a dilation interface (Homogenization.Book.Ch02.MultiscaleDilationTheory.lambdaSq_dilate) but no translation counterpart, and neither is instantiated here.

The downstream provider LambdaTransfer.lean now supplies this comparison in the forms lambda_transfer_literal and lambda_transfer_ae. To keep the dependency direction acyclic, this base module deliberately exposes the gate opening in two layers: the unconditional cube-level gate gradientW1Infinity_incrementUnitCube₂_le_of_mem_goodLocalEvent (and its two frozen-constant variants), and the conditional helpers named ..._of_lambdaTransfer, which take exactly the displayed comparison above as an explicit hypothesis. This module alone assigns no source-node status.

Main definitions #

goodLocalSensitivity: the first inequality of e.good.local.events.
goodLocalEvent: the displayed event Q(m,n,z).
goodLocalSensitivityFailure: the complement of the sensitivity clause, in the scale-resolved union form used by the proof of l.bad.event.lemma.

Main results #

mem_goodLocalEvent_iff, mem_goodLocalSensitivity_iff: the characterizations, the sensitivity clause read as the threshold bound holding at every scale L >= n.
measurableSet_goodLocalEvent.
compl_goodLocalEvent_eq, measureReal_compl_goodLocalEvent_le: the decomposition of not Q(m,n,z) used at ABK26.
gradientW1Infinity_incrementUnitCube₂_le_of_mem_goodLocalEvent and its two frozen-constant variants: the gate opening at the cube level.
lambda_sensitivity_of_mem_goodLocalEvent_of_lambdaTransfer, responseJ_sensitivity_of_mem_goodLocalEvent_of_lambdaTransfer: the two frozen sensitivity conclusions for the rescaled increment k_L - k_n, conditional on the lambda-transfer.

References #

ABK26, e.good.local.events.
ABK26, l.bad.event.lemma.
ABK26 (the two consumers).

GoodLocalEvents #

The good local sensitivity event e.good.local.events #

Reading conventions (recorded; none of them is a manuscript defect) #

The remaining input: the lambda-transfer #

Main definitions #

Main results #

References #

The sensitivity clause #

The event #

The complement decomposition of l.bad.event.lemma #

The gate opening (ABK26) #

Conditional on the lambda-transfer: the two frozen sensitivity gates #

The good local sensitivity event `e.good.local.events` #

The complement decomposition of `l.bad.event.lemma` #