CalderonZygmund

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

theorem Algsuperdiff.Frozen.External.calderon_zygmund {d : ℕ} (dimension : 2 ≤ d) (p : ENNReal) (one_lt_p : 1 < p) (p_lt_top : p < ⊤) : ∃ (C : ℝ), 0 < C ∧ ∀ (Q : HCPolySupport.TriadicCube d) (f : HCPolySupport.Vec d → HCPolySupport.Vec d), MeasureTheory.MemLp f p (HCPolySupport.normalizedCubeMeasure Q) → (∀ (u : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)), (HCPolySupport.IsZeroTraceDirichletRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet Q) u fun (x : HCPolySupport.Vec d) => -f x) → MeasureTheory.MemLp u.grad p (HCPolySupport.normalizedCubeMeasure Q) ∧ HCPolySupport.cubeLpNorm Q p u.grad ≤ C * HCPolySupport.cubeLpNorm Q p f) ∧ ∀ (u : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)), (HCPolySupport.IsMeanZeroNeumannRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet Q) u fun (x : HCPolySupport.Vec d) => -f x) → MeasureTheory.MemLp u.toH1Function.grad p (HCPolySupport.normalizedCubeMeasure Q) ∧ HCPolySupport.cubeLpNorm Q p u.toH1Function.grad ≤ C * HCPolySupport.cubeLpNorm Q p f