DeltaOsc #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The oscillation threshold delta_osc #
ABK26 introduces, in sss.bad.cubes, a strictly positive constant delta_osc
depending only on the dimension, "chosen so that the coarse-grained sensitivity
estimates (Lemmas l.lambda.sensitivity and l.J.sensitivity) can be applied
when B_osc(z + cu_j) does not occur". The manuscript's only quantitative
requirement is the displayed choice e.delta.osc.choice:
delta_osc <= 2^{-10} C_{(e.J.sensitivity.smallness.condition)}^{-1} .
Both sensitivity lemmas are frozen and proved in this repository, and both
produce their constant existentially:
Algsuperdiff.Frozen.Section24.lambda_sensitivity,
Algsuperdiff.Frozen.Section24.responseJ_sensitivity and
Algsuperdiff.Frozen.Section24.bigLambda_sensitivity each assert
exists C, 0 < C and <conditional estimate whose gate is h.gradientW1Infinity <= C^{-1} unitCubeLambda (3/8) 2 a>.
Why three Lean constants are normalized against one threshold #
One constant C, one smallness condition, two conclusions. The constant named
in e.delta.osc.choice is C_{(e.J.sensitivity.smallness.condition)} --- that
very constant --- and the surrounding sentence says delta_osc is "chosen so
that the coarse-grained sensitivity estimates (Lemmas l.lambda.sensitivity
and l.J.sensitivity) can be applied", i.e. so that both displays of
l.J.sensitivity are available on the complement of B_osc.
The Lean rendering splits the two displays into two frozen theorems, each with
its own existential constant, so the manuscript's single C becomes three
Lean constants. The faithful reading of the single-constant convention is
therefore to normalize delta_osc against all three:
deltaOsc d := 2^{-10} * (max 1 (max (max C_lambda C_J) C_BigLambda))^{-1} ,
which is the manuscript's displayed expression with all the gates merged (so
that a single threshold opens every sensitivity lemma) and clamped below 1.
All three constants, and hence deltaOsc, depend on nothing but d.
Main definitions #
lambdaSensitivityConst,responseSensitivityConst,bigLambdaSensitivityConst: the extracted frozen constants, as functions ofdalone.sensitivityConstMax: their maximum against1.deltaOsc: the manuscript'sdelta_osc.
Main results #
lambda_sensitivity_const,responseJ_sensitivity_const,bigLambda_sensitivity_const: the frozen conclusions read at the extracted constants.deltaOsc_le_two_pow_neg_ten_mul_inv_lambdaSensitivityConst,deltaOsc_le_two_pow_neg_ten_mul_inv_bigLambdaSensitivityConst: the displayed choicee.delta.osc.choice, read against thelambda- andLambda-sensitivity constants.
References #
- ABK26,
sss.bad.cubes(e.Bosc.def,e.delta.osc.choice). - ABK26,
l.lambda.sensitivity;l.J.sensitivity(one constant, one smallness conditione.J.sensitivity.smallness.condition, two displayse.J.sensitivityande.big.Lambda.sensitivity).
Extraction of the three frozen sensitivity constants #
The constant furnished by the frozen lambda-sensitivity lemma, as a
function of the dimension alone. Off the source range 2 <= d the value is
the harmless placeholder 1, which keeps the definition total without
affecting any statement below.
Equations
- Algsuperdiff.Section3.Provider.BadEvents.lambdaSensitivityConst d = if h : 2 ≤ d then Classical.choose ⋯ else 1
Instances For
The constant furnished by the frozen response-sensitivity lemma, as a function of the dimension alone.
Equations
- Algsuperdiff.Section3.Provider.BadEvents.responseSensitivityConst d = if h : 2 ≤ d then Classical.choose ⋯ else 1
Instances For
The constant furnished by the frozen Lambda-sensitivity lemma, as a
function of the dimension alone. This is the second display
e.big.Lambda.sensitivity (ABK26) of the same lemma l.J.sensitivity
that produces responseSensitivityConst; the manuscript gives the two
displays one constant, so both are normalized against the same
sensitivityConstMax below.
Equations
- Algsuperdiff.Section3.Provider.BadEvents.bigLambdaSensitivityConst d = if h : 2 ≤ d then Classical.choose ⋯ else 1
Instances For
The frozen lambda-sensitivity conclusion, read at the extracted
constant.
The frozen response-sensitivity conclusion, read at the extracted constant.
The frozen Lambda-sensitivity conclusion, read at the extracted
constant.
Positivity of the extracted lambda-sensitivity constant.
Positivity of the extracted response-sensitivity constant.
Positivity of the extracted Lambda-sensitivity constant.
The threshold #
The largest of the three sensitivity constants, clamped below by 1. This
is the single constant against which deltaOsc is normalized, so that one
threshold opens every frozen sensitivity gate.
The three-way maximum is the faithful reading of ABK26's own single-constant
convention: l.J.sensitivity states its two displays e.J.sensitivity and
e.big.Lambda.sensitivity under one constant C(d) and one smallness condition
e.J.sensitivity.smallness.condition, and it is that C which
e.delta.osc.choice names. Splitting the two displays into two frozen Lean
theorems produced two existential constants; the maximum restores the
manuscript's reading.
Equations
- One or more equations did not get rendered due to their size.
Instances For
ABK26's dimension-only oscillation threshold delta_osc
(e.Bosc.def, e.delta.osc.choice).
Equations
Instances For
The same bound against the lambda-sensitivity constant, which is what
lets a single threshold open every frozen gate.
The same bound against the Lambda-sensitivity constant, i.e. the displayed
choice e.delta.osc.choice read at the second display of l.J.sensitivity.