SuperposedFluxLowerRepresentative

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

Pointwise representative for the sharp lower coarse-ellipticity lane

The sharp superposed-flux estimate is initially simultaneous in the cutoff index only almost everywhere. This file intersects those events over the countable depth family, encloses the exceptional set in one measurable null set, and caps the random remainder by the unconditional cutoff-coercivity bound. The resulting representative is measurable, has the same weak-Orlicz tail, is uniformly bounded at every sample point, and gives the depth estimate pointwise for every cutoff index.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxSharpDepthConst {d : ℕ} (M : ABKModel d) (m : ℤ) (E : ℝ) (k : ℕ) : ℝ

The deterministic sharp prefactor at the positive-depth grid indexed by k.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxSharpDepthRare {d : ℕ} (M : ABKModel d) (E : ℝ) : ℝ

The retained rare slot for the rate-compatible integer parameters.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxSharpDepthRandom {d : ℕ} (M : ABKModel d) (m : ℤ) (E : ℝ) (k : ℕ) (omega : Cutoff.CutoffSample d) : ℝ

The raw finite-grid random remainder at positive-depth grid index k.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxSharpDepthAmp {d : ℕ} (M : ABKModel d) (m : ℤ) (E sigma : ℝ) (k : ℕ) : ℝ

The exact finite-grid weak-Orlicz amplitude of the raw remainder.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxCutoffCap {d : ℕ} (M : ABKModel d) (m : ℤ) : ℝ

An everywhere-valid deterministic cap for the normalized inverse coarse matrix at any depth and cutoff index.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxCutoffCap M m = ↑(Algsuperdiff.Section3.Annealed.sigmaBar M (m - 1)) * (4 * ↑d * M.nu⁻¹)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxCutoffCap_pos {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (m : ℤ) : 0 < superposedFluxCutoffCap M m

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.exists_superposedFluxLowerPointwiseRepresentative {d : ℕ} [NeZero d] (hd : 2 ≤ d) (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }) (hS : Frozen.Section3.inductionState M (m - 1) E) {sigma : ℝ} (hsigma : 0 < sigma) (hsigmaHalf : sigma ≤ 1 / 2) (hmax : max (Real.exp (profileAuxiliaryConst d / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E) (hEgamma : ↑E ≤ M.gamma ^ (-(1 / 5))) : ∃ (U : ℕ → Cutoff.CutoffSample d → ℝ), (∀ (n : ℕ) (omega : Cutoff.CutoffSample d), 0 ≤ U n omega) ∧ (∀ (n : ℕ), Measurable (U n)) ∧ (∀ (n : ℕ), HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 2)) (U n) (superposedFluxSharpDepthAmp M m (↑E) sigma n.pred)) ∧ (∀ (omega : Cutoff.CutoffSample d) (L : ℤ), m - 1 ≤ L → ∀ (n : ℕ), ↑(Annealed.sigmaBar M (m - 1)) * HCPolySupport.Book.Ch04.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale (HCPolySupport.originCube d m) (m - ↑n) (Cutoff.coefficientCutoff M.nu L omega) ≤ finiteQGeometricProfile (2 * superposedFluxSharpDetConst d) M.gamma n + U n omega) ∧ ∀ (n : ℕ) (omega : Cutoff.CutoffSample d), U n omega ≤ superposedFluxCutoffCap M m

One measurable representative simultaneously serves every depth and every cutoff index. The last clause is the everywhere cap that later discharges all pointwise summability requirements; it is not exported by the frozen theorem.