BadEventCoarseAssemblyFloor

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

Centered bad-event assembly at the floor-normalized coarse constant

This ordinary Provider module is the floor-normalized twin of BadEvents.BadEventCoarseAssembly. It specializes CoarseEllipticity.coarse_ellipticity_bounds_dim_floor -- the constant selection that clears the dimension floor (d : ℝ) ^ 6 as well as 1 -- at the two parameters used by the bad-event argument, and feeds those specializations into BadEventLemmaUmbrella.measureReal_compl_goodLocalEvent_le_full_reassembled. It removes that conditional A's three proof-side inputs exactly as the unnormalized assembly does:

• the centered high-branch comparison comes from ErrorComparison.lambdaSq_originCube_eighth_le by inversion;
• the high-branch lower-family estimate is the floor-normalized coarse theorem at s = 1/8;
• the low-branch family of translated estimates comes from the same theorem at s = 1/16 through ObservableSwapPayoff.isLowerIntegerFamilyOrlicz_cubeLowerEllipticityInv_forall_descendant.

The output is centered at originCube d m, carries the extra conjunct (d : ℝ) ^ 6 ≤ Cbase, and retains precisely the two branch implications of the non-linear-term bound. Translation of the whole good-local-event probability to the paper's arbitrary spatial translate is outside this module: it is performed by the frozen successor Algsuperdiff.Frozen.Section3.bad_event_estimate, whose proof engine this module is.

References

• ABK26, l.bad.event.lemma, statement; e.good.local.events; p.cg.ellipticity.bounds.

noncomputable def Algsuperdiff.Section3.Provider.BadEvents.badEventCoarseAdmissibleConstFloor (d : ℕ) (Ccg : ℝ) : ℝ

A source-admissibility choice large enough for both the full oscillation argument and the two floor-normalized coarse-ellipticity specializations. The factor 3 / 2 is the model-independent upper bound for cstar; the two entries in the inner maximum respectively open the frozen maximum gate at sigma = 1/2 and make the rare scale at most 1/64.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.BadEvents.badEventCoarseAdmissibleConstFloor_pos (d : ℕ) {Ccg : ℝ} (hCcg : 0 < Ccg) : 0 < badEventCoarseAdmissibleConstFloor d Ccg

Positivity of the combined admissibility constant.

theorem Algsuperdiff.Section3.Provider.BadEvents.exists_measureReal_compl_goodLocalEvent_originCube_le_of_frozenCoarse_dimFloor (d : ℕ) : ∃ (Cbase : ℝ), 1 ≤ Cbase ∧ ↑d ^ 6 ≤ Cbase ∧ ∀ (M : ABKModel d) (m n m0 : ℤ) (E : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M (m0 - 1) E → n ≤ m0 - 1 → badEventCoarseAdmissibleConstFloor d Cbase ≤ ↑E * Disorder.cstar M → M.gamma ≤ ↑E ^ (-5) → (n < m → 1 ≤ badEventOscFullRate M (2 * Cbase) (HCPolySupport.originCube d m) n) → (n < m → ↑d * (↑m - ↑n) * Real.log 3 + Real.exp (1 / 8 * (Cbase⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)) ≤ Real.exp (1 / 4 * (Cbase⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) → (↑(Cutoff.cutoffSampleLaw M)).real (goodLocalEvent M (2 * Cbase) (HCPolySupport.originCube d m) n)ᶜ ≤ Real.exp (-badEventOscFullRate M (2 * Cbase) (HCPolySupport.originCube d m) n) + Real.exp (-Real.exp (1 / 8 * (Cbase⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)))

The centered bad-event umbrella at the floor-normalized constant. The floor-normalized coarse theorem supplies both ellipticity branches, and the selected constant Cbase carries 1 ≤ Cbase together with the dimension floor (d : ℝ) ^ 6 ≤ Cbase. The only branch-specific assumptions left to the caller are the two non-linear-term implications.