A uniform bound for the Cauchy transform of compactly supported $L^p$ data, $p>2$

import Definitions.Def_JHolomorphic_Setting
import Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
import Mathlib.MeasureTheory.Constructions.HaarToSphere
import Mathlib.MeasureTheory.Measure.Lebesgue.Complex
import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
import Mathlib.MeasureTheory.Measure.Haar.Unique
import Mathlib.MeasureTheory.Group.Measure
import Mathlib.Analysis.SpecialFunctions.Integrability.Basic
import Mathlib.LinearAlgebra.Complex.FiniteDimensional

namespace JHolomorphic

open MeasureTheory Metric Filter Topology Set
open scoped ContDiff ENNReal NNReal

/-- Let `2 < p < ∞` and `R > 0`. There is `C ≥ 0` such that for every `g ∈ L^p(ℂ; E)` vanishing
outside the disc `B_R(0)` and every `z ∈ B_R(0)`, the map `ζ ↦ (z - ζ)⁻¹ g(ζ)` is integrable and
`‖∫ (z - ζ)⁻¹ g(ζ) dζ‖ ≤ C ‖g‖_{L^p}`. -/
theorem norm_integral_inv_sub_smul_le {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
    (p R : ℝ) (hp : 2 < p) (hR : 0 < R) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ g : ℂ → E, MemLp g (ENNReal.ofReal p) volume →
      Function.support g ⊆ ball 0 R → ∀ z ∈ ball (0 : ℂ) R,
        Integrable (fun ζ => (z - ζ)⁻¹ • g ζ) ∧
        ‖∫ ζ, (z - ζ)⁻¹ • g ζ‖ ≤ C * (eLpNorm g (ENNReal.ofReal p) volume).toReal := by
  sorry

end JHolomorphic