CubeSchauder

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

theorem Algsuperdiff.Frozen.External.cube_schauder {d : ℕ} (dimension : 2 ≤ d) (s : ℝ) (s_pos : 0 < s) (s_le : s ≤ 1 / 2) : ∃ (C : ℝ), 0 < C ∧ ∀ (m : ℤ) (sigma : ℝ), 0 < sigma → ∀ (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (Kg KhInf Kh : ℝ), Section4.Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g → (∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖h.grad x‖ ≤ KhInf) → Section4.Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kh h.grad → ∃ (v : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))), Section4.Support.IsDirichletSolutionOn (fun (x : HCPolySupport.Vec d) => sigma • 1) (HCPolySupport.originCube d m) v h g ∧ ∃ (Ksup : ℝ) (KHol : ℝ), 0 ≤ Ksup ∧ 0 ≤ KHol ∧ (∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖v.grad x‖ ≤ Ksup) ∧ Section4.Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s KHol v.grad ∧ Real.rpow 3 (-(s * ↑m)) * Ksup + KHol ≤ C * (Real.rpow 3 (s * ↑m))⁻¹ * (sigma⁻¹ * Real.rpow 3 (↑m / 2) * Kg + (KhInf + Real.rpow 3 (↑m / 2) * Kh))