SuperposedFluxLowerProvider

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

Sharp superposed-flux provider for the lower coarse-ellipticity leg

The earlier local-payoff interface factors 3^(2 * beta * k₀) into a common constant. That factor is harmless only in the collar term, where it remains paired with the rare factor exp (-kp / 36); putting it into the deterministic term loses the dimension-only profile as gamma tends to zero. This file keeps the collar factor in the rare slot and builds the lower provider from that sharp split.

The sharp local split

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxSharpConst {d : ℕ} (M : ABKModel d) (n i : ℤ) (eps beta : ℝ) (k₀ kp : ℕ) : ℝ

The deterministic part of the shifted pure-flux constant. Only the (2 gamma + eps) * k₀ shift belongs here.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxSharpRare (beta : ℝ) (k₀ kp : ℕ) : ℝ

The collar shift retained beside the rare factor.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxSharpRare beta k₀ kp = 3 ^ (2 * beta * ↑k₀) * Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxRare kp

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxSharpConst_pos {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (n i : ℤ) (eps beta : ℝ) (k₀ kp : ℕ) : 0 < superposedFluxSharpConst M n i eps beta k₀ kp

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxSharpRare_pos (beta : ℝ) (k₀ kp : ℕ) : 0 < superposedFluxSharpRare beta k₀ kp

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.sum_superposedConclusionPayload_flux_basis_le_sharpStep3Payload {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (n i L : ℤ) (E : ℝ) {b eps beta : ℝ} (heps : 0 < eps) (hbetab : 2 * b + 2 * M.gamma + eps ≤ 2 * beta) (t : ℝ) (k₀ kp : ℕ) (omega : Cutoff.CutoffSample d) : ∑ j : Fin d, Multiscale.superposedConclusionPayload M n i L E b eps t beta k₀ kp omega 0 (HCPolySupport.basisVec j) ≤ superposedFluxSharpConst M n i eps beta k₀ kp * (3 ^ (superposedFluxLocalExponent M b eps beta * ↑(Percolation.hsep M n E b omega)) * (1 + 3 ^ (2 * b * ↑(Percolation.hsep M n E b omega)) * superposedFluxSharpRare beta k₀ kp))

The pure-flux conclusion with the collar shift left in its rare slot.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.slstar_local_perCube_of_sharpSuperposedFluxConclusion_ae {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M (m - 1) E) {b : ℝ} (hb0 : 0 < b) (hb : b ≤ 1 / 8) {k₀ : ℕ} (hk₀ : 3 ≤ k₀) {eps : ℝ} (heps : 0 < eps) {t : ℝ} (ht0 : 0 ≤ t) {beta : ℝ} (hbeta0 : 0 < beta) (hbeta9 : 9 * beta ≤ 1) (hbetab : 2 * b + 2 * M.gamma + eps ≤ 2 * beta) (hgammaWin : 4 * (2 * M.gamma + eps) ≤ 1 - beta) {kp : ℕ} (hcap : 9 * 99 ^ d * (Real.exp (-(Percolation.siteRateBase d / 2 * ((↑E)⁻¹ ^ 2 * M.gamma⁻¹))) + 3 ^ (-(↑k₀ / 2))) ≤ Real.exp (-↑kp)) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), (Percolation.hsepSet M R.scale (↑E) b (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega)).Nonempty → ∀ (L : ℤ), m - 1 ≤ L → (∀ (n : ℕ), ∀ Q ∈ Whitney.whitneyLayer R.scale (Whitney.whitneyScale M R.scale (↑E) b k₀ (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega)) n, Stream.cubeSupBound Q Q.scale L ↑(Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega) ≤ Multiscale.whitneyWaveLayerScale M R.scale (Whitney.whitneyScale M R.scale (↑E) b k₀ (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega)) n L * t) → cutoffSigmaStarInvBlockFamily M L (↑(Annealed.sigmaBar M (m - 1))) R omega ≤ 2 * superposedFluxSharpConst M R.scale (m - 1) eps beta k₀ kp + Multiscale.bfaLocalLane M R (↑E) b (superposedFluxLocalExponent M b eps beta) (superposedFluxSharpConst M R.scale (m - 1) eps beta k₀ kp) (superposedFluxSharpRare beta k₀ kp) omega

Conditional one-cube payoff with the sharp deterministic and rare slots.

Removal of the translated wave and separation gates

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.slstar_local_perCube_allL_ae_sharp_of_gates {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M (m - 1) E) {sigma b : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hEexp : Real.exp (Percolation.badClustersConst d / sigma) ≤ ↑E) (hE4 : 4 ≤ ↑E) (hunit : BadEvents.unitGate M) (hgamma20 : M.gamma ≤ 1 / 20) (hinvSq : (↑E)⁻¹ ^ 2 ≤ Disorder.cstar M) (hEb : Percolation.badClustersConst d / b ≤ ↑E) (hgamma : M.gamma ≤ ↑E ^ (-5)) {k₀ : ℕ} (hk₀ : 3 ≤ k₀) {eps : ℝ} (heps : 0 < eps) {beta : ℝ} (hbeta0 : 0 < beta) (hbeta9 : 9 * beta ≤ 1) (hbetab : 2 * b + 2 * M.gamma + eps ≤ 2 * beta) (hgammaWin : 4 * (2 * M.gamma + eps) ≤ 1 - beta) {kp : ℕ} (hcap : 9 * 99 ^ d * (Real.exp (-(Percolation.siteRateBase d / 2 * ((↑E)⁻¹ ^ 2 * M.gamma⁻¹))) + 3 ^ (-(↑k₀ / 2))) ≤ Real.exp (-↑kp)) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∀ (L : ℤ), m - 1 ≤ L → cutoffSigmaStarInvBlockFamily M L (↑(Annealed.sigmaBar M (m - 1))) R omega ≤ 2 * superposedFluxSharpConst M R.scale (m - 1) eps beta k₀ kp + Multiscale.bfaLocalLane M R (↑E) b (superposedFluxLocalExponent M b eps beta) (superposedFluxSharpConst M R.scale (m - 1) eps beta k₀ kp) (superposedFluxSharpRare beta k₀ kp) omega

The sharp one-cube payoff holds almost surely for every cutoff index.

Finite descendant-grid lift

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.slstar_descendantGrid_allL_ae_sharp_of_gates {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m : ℤ} (k : ℕ) {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M (m - 1) E) {sigma b : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hEexp : Real.exp (Percolation.badClustersConst d / sigma) ≤ ↑E) (hE4 : 4 ≤ ↑E) (hunit : BadEvents.unitGate M) (hgamma20 : M.gamma ≤ 1 / 20) (hinvSq : (↑E)⁻¹ ^ 2 ≤ Disorder.cstar M) (hEb : Percolation.badClustersConst d / b ≤ ↑E) (hgamma : M.gamma ≤ ↑E ^ (-5)) {k₀ : ℕ} (hk₀ : 3 ≤ k₀) {eps : ℝ} (heps : 0 < eps) {beta : ℝ} (hbeta0 : 0 < beta) (hbeta9 : 9 * beta ≤ 1) (hbetab : 2 * b + 2 * M.gamma + eps ≤ 2 * beta) (hgammaWin : 4 * (2 * M.gamma + eps) ≤ 1 - beta) {kp : ℕ} (hcap : 9 * 99 ^ d * (Real.exp (-(Percolation.siteRateBase d / 2 * ((↑E)⁻¹ ^ 2 * M.gamma⁻¹))) + 3 ^ (-(↑k₀ / 2))) ≤ Real.exp (-↑kp)) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∀ R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k), ∀ (L : ℤ), m - 1 ≤ L → cutoffSigmaStarInvBlockFamily M L (↑(Annealed.sigmaBar M (m - 1))) R omega ≤ 2 * superposedFluxSharpConst M (m - 1 - ↑k) (m - 1) eps beta k₀ kp + Multiscale.bfaLocalGridSup M m k (↑E) b (superposedFluxLocalExponent M b eps beta) (superposedFluxSharpConst M (m - 1 - ↑k) (m - 1) eps beta k₀ kp) (superposedFluxSharpRare beta k₀ kp) omega

The sharp payoff simultaneously over the finite descendant grid.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.slstar_descendantGrid_allL_ae_and_isBigOWith_sharp_of_gates {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m : ℤ} (k : ℕ) {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M (m - 1) E) {sigma b : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hEexp : Real.exp (Percolation.badClustersConst d / sigma) ≤ ↑E) (hE4 : 4 ≤ ↑E) (hunit : BadEvents.unitGate M) (hgamma20 : M.gamma ≤ 1 / 20) (hinvSq : (↑E)⁻¹ ^ 2 ≤ Disorder.cstar M) (hEb : Percolation.badClustersConst d / b ≤ ↑E) (hgamma : M.gamma ≤ ↑E ^ (-5)) {k₀ : ℕ} (hk₀ : 3 ≤ k₀) {eps : ℝ} (heps : 0 < eps) {beta : ℝ} (hbeta0 : 0 < beta) (hbeta9 : 9 * beta ≤ 1) (hbetab : 2 * b + 2 * M.gamma + eps ≤ 2 * beta) (hgammaWin : 4 * (2 * M.gamma + eps) ≤ 1 - beta) {kp : ℕ} (hcap : 9 * 99 ^ d * (Real.exp (-(Percolation.siteRateBase d / 2 * ((↑E)⁻¹ ^ 2 * M.gamma⁻¹))) + 3 ^ (-(↑k₀ / 2))) ≤ Real.exp (-↑kp)) (hlocalb : superposedFluxLocalExponent M b eps beta ≤ b) : (∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∀ R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k), ∀ (L : ℤ), m - 1 ≤ L → cutoffSigmaStarInvBlockFamily M L (↑(Annealed.sigmaBar M (m - 1))) R omega ≤ 2 * superposedFluxSharpConst M (m - 1 - ↑k) (m - 1) eps beta k₀ kp + Multiscale.bfaLocalGridSup M m k (↑E) b (superposedFluxLocalExponent M b eps beta) (superposedFluxSharpConst M (m - 1 - ↑k) (m - 1) eps beta k₀ kp) (superposedFluxSharpRare beta k₀ kp) omega) ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma (Multiscale.bfaTau sigma (superposedFluxLocalExponent M b eps beta) b)) (Multiscale.bfaLocalGridSup M m k (↑E) b (superposedFluxLocalExponent M b eps beta) (superposedFluxSharpConst M (m - 1 - ↑k) (m - 1) eps beta k₀ kp) (superposedFluxSharpRare beta k₀ kp)) (gridBlockAmp d (Multiscale.bfaTau sigma (superposedFluxLocalExponent M b eps beta) b) (Multiscale.bfaLaneScale sigma b (superposedFluxLocalExponent M b eps beta) (superposedFluxSharpConst M (m - 1 - ↑k) (m - 1) eps beta k₀ kp) (superposedFluxSharpRare beta k₀ kp)) k)

The sharp grid payoff paired with its direct Orlicz certificate.

Dimension-only deterministic profile

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxKBase (d : ℕ) : ℝ

The pure-flux value of the Ktot prefactor, before its scale power.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxKBase d = 960 * Algsuperdiff.Section3.Provider.Multiscale.simplexCrudeConst d (1 / 4)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.ktotConst_flux_basis_eq {d : ℕ} (M : ABKModel d) (n i : ℤ) (j : Fin d) : Multiscale.ktotConst M n i 3 0 0 (HCPolySupport.basisVec j) = superposedFluxKBase d * 3 ^ (M.gamma * (↑i - ↑n))

The pure-flux Ktot constant is the dimension-only base times its scale power.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxSharpDetConst (d : ℕ) : ℝ

A dimension-only envelope for the sharp deterministic constant.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxSharpDetConst_pos {d : ℕ} (hd : 2 ≤ d) : 0 < superposedFluxSharpDetConst d