EdBridgeStepFourGeneral

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

1. The bridge's constants at a general Schauder constant

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.edBridgeRemWeightGen (d : ℕ) (Cs : ℝ) (k : ℕ) : ℝ

The one-step remainder's weight at a general Schauder constant Cs: C_r(d, Cs, k) · √((3²)^d). At Cs = schauderWindowConst d this is edBridgeRemWeight.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.edBridgeRemWeightGen d Cs k = Algsuperdiff.Section4.Provider.ExcessDecay.triangleRemainderConst d Cs k * √((3 ^ 2) ^ d)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.edBridgeRemWeightGen_nonneg (d : ℕ) {Cs : ℝ} (hCs : 0 ≤ Cs) (k : ℕ) : 0 ≤ edBridgeRemWeightGen d Cs k

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.edBridgeEpsConstGen (d : ℕ) (Cs C : ℝ) (k : ℕ) : ℝ

The ε constant of the bridge at a general Schauder constant Cs.

Equations

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

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_edBridgeStepGen (d : ℕ) (Cs : ℝ) : ∃ (k₀ : ℕ), 3 ≤ k₀ ∧ ∀ (k : ℕ), k₀ ≤ k → taylorContractionConst d * Cs * windowRatioConst d 2 * windowRatioConst d 1 * (3 ^ (-↑k)) ^ (1 / 2) ≤ 1 / 2 * 3 ^ (-(1 / 4) * (↑k + 1))

** residue 4 at a general Schauder constant.**

EdBridgeFolds.exists_edBridgeStep with schauderWindowConst d replaced by an arbitrary Cs: the step size k₀ depends on Cs, nothing else in the argument does. The join runs at Cs = max (schauderWindowConst d) C_bdry.