StepSevenFlushAssembly

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

1. The two exponent facts

theorem Algsuperdiff.Section4.Provider.Regularity.flush_exponent_gag {n m : ℤ} (hnm : n + 3 ≤ m) : Real.rpow 3 (stepOneS * ↑(n + 2)) * 3 ^ (↑(n + 3) / 4) ≤ Real.rpow 3 (↑m / 2)

3^{s(n+2)}·3^{(n+3)/4} ≤ 3^{m/2} at s = 1/4, for n+3 ≤ m — item 1(b), proved.

theorem Algsuperdiff.Section4.Provider.Regularity.flush_exponent_gag_low {n m : ℤ} (hnm : n + 3 ≤ m) : Real.rpow 3 (-↑(n + 2)) * Real.rpow 3 ((1 + stepOneS) * ↑n) * 3 ^ (↑(n + 3) / 4) ≤ Real.rpow 3 (↑m / 2)

3^{-(n+2)}·3^{(1+s)n}·3^{(n+3)/4} ≤ 3^{m/2} at s = 1/4, for n+3 ≤ m.

theorem Algsuperdiff.Section4.Provider.Regularity.flush_exponent_flat {n : ℤ} : Real.rpow 3 (-↑(n + 2)) * Real.rpow 3 ↑n ≤ 1

3^{-(n+2)}·3^{n} = 3^{-2} ≤ 1.

theorem Algsuperdiff.Section4.Provider.Regularity.rpow_neg_succ_eq_three_mul {n : ℤ} : Real.rpow 3 (-↑(n + 2)) = 3 * 3 ^ (-(n + 3))

The rpow → zpow splitting 3^{-(n+2)} = 3·3^{-(n+3)}.

2. The flush constant

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepSevenFlushCG (d : ℕ) (K2 : ℝ) : ℝ

The flush branch's 𝐠-leg constant.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepSevenFlushCH (d : ℕ) (K2 : ℝ) : ℝ

The flush branch's ∇h-leg constant.

Equations

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

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenFlushCG_nonneg (d : ℕ) {K2 : ℝ} (hK2 : 0 ≤ K2) : 0 ≤ stepSevenFlushCG d K2

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenFlushCH_nonneg (d : ℕ) {K2 : ℝ} (hK2 : 0 ≤ K2) : 0 ≤ stepSevenFlushCH d K2

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepSevenFlushCg (d : ℕ) (K1 K2 Cosc : ℝ) : ℝ

The flush branch's hgrad-slot constant.

Equations

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

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenFlushCg_nonneg (d : ℕ) {K1 K2 Cosc : ℝ} (hK1 : 0 ≤ K1) (hK2 : 0 ≤ K2) (hCosc : 0 ≤ Cosc) : 0 ≤ stepSevenFlushCg d K1 K2 Cosc

3. The bracket pricing

theorem Algsuperdiff.Section4.Provider.Regularity.flushBracket_le {d : ℕ} {m n : ℤ} {z : HCPolySupport.Vec d} {sigma K2 Khol Kh : ℝ} (uglob hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) {gsrc : HCPolySupport.Vec d → HCPolySupport.Vec d} (hd1 : 1 ≤ d) (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hnm : n + 3 ≤ m) (hsigma : 0 < sigma) (hK2 : 0 ≤ K2) (hKhol : 0 ≤ Khol) (hKh : 0 ≤ Kh) (hgHol : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Khol gsrc) (hhHol : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kh hdat.grad) (hsup : ∀ y ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖hdat.grad y‖ ≤ Real.rpow 3 (↑m / 2) * Kh) : √sigma * Real.rpow 3 (-↑(n + 2)) * (MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => uglob.toFun y - HCPolySupport.volumeAverage (ExcessDecay.truncatedWindow z m (n + 3)) uglob.toFun) 2 (Support.normalizedVolumeMeasureOn (ExcessDecay.truncatedWindow z m (n + 3)))).toReal + √sigma * Real.rpow 3 (-↑(n + 2)) * (K2 * ((MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => uglob.toFun y - HCPolySupport.volumeAverage (ExcessDecay.truncatedWindow z m (n + 3)) uglob.toFun) 2 (Support.normalizedVolumeMeasureOn (ExcessDecay.truncatedWindow z m (n + 3)))).toReal + 3 ^ n * ∑ i' : Fin d, (MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => hdat.grad y i') 2 (Support.normalizedVolumeMeasureOn (ExcessDecay.truncatedWindow z m (n + 3)))).toReal + stepOneS.rpow (-6) * Real.rpow 3 ↑n * (MeasureTheory.eLpNorm hdat.grad 2 (Support.normalizedVolumeMeasureOn (ExcessDecay.truncatedWindow z m (n + 3)))).toReal + stepOneS.rpow (-6) * Real.rpow 3 ((1 + stepOneS) * ↑n) * (Support.normalizedGagliardoESeminormOn (ExcessDecay.truncatedWindow z m (n + 3)) stepOneS hdat.grad).toReal + stepOneS.rpow (-7) * sigma⁻¹ * Real.rpow 3 ((1 + stepOneS) * ↑n) * (Support.normalizedGagliardoESeminormOn (ExcessDecay.truncatedWindow z m (n + 3)) stepOneS gsrc).toReal)) + stepOneS.rpow (-3) * √sigma⁻¹ * Real.rpow 3 (stepOneS * ↑(n + 2)) * (Support.normalizedGagliardoESeminormOn (ExcessDecay.truncatedWindow z m (n + 3)) stepOneS gsrc).toReal + stepOneS.rpow (-2) * √sigma * Real.rpow 3 (stepOneS * ↑(n + 2)) * (Support.normalizedGagliardoESeminormOn (ExcessDecay.truncatedWindow z m (n + 3)) stepOneS hdat.grad).toReal + stepOneS.rpow (-2) * √sigma * (MeasureTheory.eLpNorm hdat.grad 2 (Support.normalizedVolumeMeasureOn (ExcessDecay.truncatedWindow z m (n + 3)))).toReal ≤ 3 * (1 + K2) * (√sigma * (3 ^ (-(n + 3)) * Support.normalizedL2On (ExcessDecay.truncatedWindow z m (n + 3)) fun (y : HCPolySupport.Vec d) => uglob.toFun y - HCPolySupport.volumeAverage (ExcessDecay.truncatedWindow z m (n + 3)) uglob.toFun)) + stepSevenFlushCG d K2 * (√sigma⁻¹ * (Real.rpow 3 (↑m / 2) * Khol)) + stepSevenFlushCH d K2 * (√sigma * (Real.rpow 3 (↑m / 2) * Kh))

The flush bracket, priced onto the display carriers.