HomStepFourSchauder

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

Theorem B, §4.5: the hSch discharge off the external Schauder input

What this is

The definitional bridge from the external classical input Algsuperdiff.Frozen.External.cube_schauder (proved internally in this repository) to the three Schauder slots of stepFourEnergyDisplay/stepFourEnergyEndpoint: the comparator's existence, the gradient sup bound hb, the gradient Hölder bound hH, and the gauge estimate hSch — with the constant Csch = C(d, s) produced ONCE, before the scale m, the diffusivity sigma and the data, so the consumer's constant scope is the external's own.

The inequality transfer is definitional: wsInftyGauge (originCube d m) and dataBracket unfold to exactly the primitive terms of the external's conclusion (the cube's scale is m by rfl).

Axiom status

The external input is proved, with axioms exactly [propext, Classical.choice, Quot.sound] and no sorryAx, so every consumer of this module sees the standard axiom triple only.

theorem Algsuperdiff.Section4.Provider.Homogenization.exists_comparator_schauder_package {d : ℕ} (dimension : 2 ≤ d) {s : ℝ} (s_pos : 0 < s) (s_le : s ≤ 1 / 2) : ∃ (Csch : ℝ), 0 < Csch ∧ ∀ (m : ℤ) (sigma : ℝ), 0 < sigma → ∀ (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (Kg KhInf Kh : ℝ), Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g → (∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖h.grad x‖ ≤ KhInf) → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kh h.grad → ∃ (v : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))), 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) ∧ Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s KHol v.grad ∧ wsInftyGauge (HCPolySupport.originCube d m) s Ksup KHol ≤ Csch * (Real.rpow 3 (s * ↑m))⁻¹ * dataBracket sigma (Real.rpow 3 (↑m / 2)) Kg KhInf Kh

The comparator with its Schauder package, off the external input.

One constant Csch(d, s) for every scale, diffusivity and admissible data: the solution v of -sigma Δv = ∇·g, v = h on ∂□_m, exists with its own gradient representative bounded (hb), s-Hölder (hH), and gauge-controlled by the data bracket (hSch) — the three slots of stepFourEnergyEndpoint.