Bounded Cauchy differentiation between closed disks

The operator integrates on a circle of radius σ - ρ centered at each point of the smaller disk. It is defined on all continuous outer-disk functions; on holomorphic inputs it agrees with the actual complex derivative.

@[reducible, inline]

abbrev NavierStokes.CauchyRestriction.Disk (c : ℂ) (r : ℝ) : Type

Disk: an abbreviation for ↥(closedBall c r).

Equations

• NavierStokes.CauchyRestriction.Disk c r = ↑(Metric.closedBall c r)

instance NavierStokes.CauchyRestriction.diskCompactSpace (c : ℂ) (r : ℝ) : CompactSpace (Disk c r)

noncomputable def NavierStokes.CauchyRestriction.inclusion (c : ℂ) {ρ σ : ℝ} (h : ρ ≤ σ) : C(Disk c ρ, Disk c σ)

Inclusion, bundling toFun, continuous_toFun.

Equations

• NavierStokes.CauchyRestriction.inclusion c h = { toFun := fun (z : NavierStokes.CauchyRestriction.Disk c ρ) => ⟨↑z, ⋯⟩, continuous_toFun := ⋯ }

noncomputable def NavierStokes.CauchyRestriction.restrictionLinear {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ℂ) {ρ σ : ℝ} (h : ρ ≤ σ) : C(Disk c σ, E) →ₗ[ℂ] C(Disk c ρ, E)

Restriction linear, bundling toFun, map_add, map_smul.

Equations

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

theorem NavierStokes.CauchyRestriction.norm_restrictionLinear_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ℂ) {ρ σ : ℝ} (h : ρ ≤ σ) (f : C(Disk c σ, E)) : ‖(restrictionLinear c h) f‖ ≤ ‖f‖

noncomputable def NavierStokes.CauchyRestriction.restrictionCLM {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ℂ) {ρ σ : ℝ} (h : ρ ≤ σ) : C(Disk c σ, E) →L[ℂ] C(Disk c ρ, E)

Restriction continuous linear map, given by (restrictionLinear c h).mkContinuous 1 (by intro f simpa only [one_mul] using norm_restrictionLinear_le c h f).

Equations

• NavierStokes.CauchyRestriction.restrictionCLM c h = (NavierStokes.CauchyRestriction.restrictionLinear c h).mkContinuous 1 ⋯

@[simp]

theorem NavierStokes.CauchyRestriction.restrictionCLM_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ℂ) {ρ σ : ℝ} (h : ρ ≤ σ) (f : C(Disk c σ, E)) (z : Disk c ρ) : ((restrictionCLM c h) f) z = f ⟨↑z, ⋯⟩

theorem NavierStokes.CauchyRestriction.restrictionCLM_comp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ℂ) {r ρ σ : ℝ} (h₁ : r ≤ ρ) (h₂ : ρ ≤ σ) : restrictionCLM c h₁ ∘SL restrictionCLM c h₂ = restrictionCLM c ⋯

theorem NavierStokes.CauchyRestriction.offset_ne_zero {δ : ℝ} (hδ : 0 < δ) (θ : ℝ) : circleMap 0 δ θ ≠ 0

theorem NavierStokes.CauchyRestriction.translated_mem (c : ℂ) {ρ σ : ℝ} (hgap : ρ < σ) (z : Disk c ρ) (θ : ℝ) : ↑z + circleMap 0 (σ - ρ) θ ∈ Metric.closedBall c σ

noncomputable def NavierStokes.CauchyRestriction.sample (c : ℂ) {ρ σ : ℝ} (hgap : ρ < σ) (θ : ℝ) : C(Disk c ρ, Disk c σ)

Sample, bundling toFun, continuous_toFun.

Equations

• NavierStokes.CauchyRestriction.sample c hgap θ = { toFun := fun (z : NavierStokes.CauchyRestriction.Disk c ρ) => ⟨↑z + circleMap 0 (σ - ρ) θ, ⋯⟩, continuous_toFun := ⋯ }

noncomputable def NavierStokes.CauchyRestriction.weight (δ θ : ℝ) : ℂ

Weight, given by I / circleMap 0 δ θ.

Equations

• NavierStokes.CauchyRestriction.weight δ θ = Complex.I / circleMap 0 δ θ

theorem NavierStokes.CauchyRestriction.continuous_weight {δ : ℝ} (hδ : 0 < δ) : Continuous (weight δ)

theorem NavierStokes.CauchyRestriction.norm_weight {δ : ℝ} (hδ : 0 < δ) (θ : ℝ) : ‖weight δ θ‖ = δ⁻¹

noncomputable def NavierStokes.CauchyRestriction.integrand {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ℂ) {ρ σ : ℝ} (hgap : ρ < σ) (f : C(Disk c σ, E)) (θ : ℝ) : C(Disk c ρ, E)

Integrand, given by weight (σ - ρ) θ • f.comp (sample c hgap θ).

Equations

• NavierStokes.CauchyRestriction.integrand c hgap f θ = NavierStokes.CauchyRestriction.weight (σ - ρ) θ • f.comp (NavierStokes.CauchyRestriction.sample c hgap θ)

theorem NavierStokes.CauchyRestriction.continuous_integrand {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ℂ) {ρ σ : ℝ} (hgap : ρ < σ) (f : C(Disk c σ, E)) : Continuous (integrand c hgap f)

theorem NavierStokes.CauchyRestriction.norm_integrand_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ℂ) {ρ σ : ℝ} (hgap : ρ < σ) (f : C(Disk c σ, E)) (θ : ℝ) : ‖integrand c hgap f θ‖ ≤ (σ - ρ)⁻¹ * ‖f‖

noncomputable def NavierStokes.CauchyRestriction.cauchyMap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ℂ) {ρ σ : ℝ} (hgap : ρ < σ) (f : C(Disk c σ, E)) : C(Disk c ρ, E)

Cauchy map, given by (2 * Real.pi * I : ℂ)⁻¹ • ∫ θ : ℝ in (0)..(2 * Real.pi), integrand c hgap f θ.

Equations

• NavierStokes.CauchyRestriction.cauchyMap c hgap f = (2 * ↑Real.pi * Complex.I)⁻¹ • ∫ (θ : ℝ) in 0..2 * Real.pi, NavierStokes.CauchyRestriction.integrand c hgap f θ

theorem NavierStokes.CauchyRestriction.cauchyMap_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ℂ) {ρ σ : ℝ} (hgap : ρ < σ) (f g : C(Disk c σ, E)) : cauchyMap c hgap (f + g) = cauchyMap c hgap f + cauchyMap c hgap g

theorem NavierStokes.CauchyRestriction.cauchyMap_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ℂ) {ρ σ : ℝ} (hgap : ρ < σ) (a : ℂ) (f : C(Disk c σ, E)) : cauchyMap c hgap (a • f) = a • cauchyMap c hgap f

theorem NavierStokes.CauchyRestriction.norm_cauchyMap_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ℂ) {ρ σ : ℝ} (hgap : ρ < σ) (f : C(Disk c σ, E)) : ‖cauchyMap c hgap f‖ ≤ (σ - ρ)⁻¹ * ‖f‖

noncomputable def NavierStokes.CauchyRestriction.derivativeCLM {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ℂ) {ρ σ : ℝ} (hgap : ρ < σ) : C(Disk c σ, E) →L[ℂ] C(Disk c ρ, E)

Derivative continuous linear map as an element of C(Disk c σ, E) →L[ℂ] C(Disk c ρ, E).

Equations

• NavierStokes.CauchyRestriction.derivativeCLM c hgap = { toFun := NavierStokes.CauchyRestriction.cauchyMap c hgap, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (σ - ρ)⁻¹ ⋯

theorem NavierStokes.CauchyRestriction.norm_derivativeCLM_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ℂ) {ρ σ : ℝ} (hgap : ρ < σ) : ‖derivativeCLM c hgap‖ ≤ (σ - ρ)⁻¹

theorem NavierStokes.CauchyRestriction.norm_restrictionCLM_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ℂ) {ρ σ : ℝ} (h : ρ ≤ σ) : ‖restrictionCLM c h‖ ≤ 1

theorem NavierStokes.CauchyRestriction.derivativeCLM_apply_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (c : ℂ) {ρ σ : ℝ} (hgap : ρ < σ) (f : C(Disk c σ, E)) (z : Disk c ρ) : ((derivativeCLM c hgap) f) z = (2 * ↑Real.pi * Complex.I)⁻¹ • ∫ (θ : ℝ) in 0..2 * Real.pi, weight (σ - ρ) θ • f ((sample c hgap θ) z)

theorem NavierStokes.CauchyRestriction.ball_subset_outer (c : ℂ) {ρ σ : ℝ} (z : Disk c ρ) : Metric.ball (↑z) (σ - ρ) ⊆ Metric.ball c σ

theorem NavierStokes.CauchyRestriction.circle_kernel_identity {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {δ : ℝ} (hδ : 0 < δ) (z : ℂ) (θ : ℝ) (v : E) : weight δ θ • v = deriv (circleMap z δ) θ • (circleMap z δ θ - z) ^ (-2) • v

theorem NavierStokes.CauchyRestriction.derivativeCLM_apply_of_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (c : ℂ) {ρ σ : ℝ} (hgap : ρ < σ) (f : C(Disk c σ, E)) (F : ℂ → E) (hF : DiffContOnCl ℂ F (Metric.ball c σ)) (hvalues : ∀ (w : Disk c σ), f w = F ↑w) (z : Disk c ρ) : ((derivativeCLM c hgap) f) z = deriv F ↑z

Use any holomorphic extension agreeing with the continuous outer-disk input.

noncomputable def NavierStokes.CauchyRestriction.ofContinuousOn {E : Type u_1} [NormedAddCommGroup E] (c : ℂ) (r : ℝ) (F : ℂ → E) (hF : ContinuousOn F (Metric.closedBall c r)) : C(Disk c r, E)

Of continuous on, given by ⟨fun z => F z, hF.domRestrict⟩.

Equations

• NavierStokes.CauchyRestriction.ofContinuousOn c r F hF = { toFun := fun (z : NavierStokes.CauchyRestriction.Disk c r) => F ↑z, continuous_toFun := ⋯ }

@[simp]

theorem NavierStokes.CauchyRestriction.ofContinuousOn_apply {E : Type u_1} [NormedAddCommGroup E] (c : ℂ) (r : ℝ) (F : ℂ → E) (hF : ContinuousOn F (Metric.closedBall c r)) (z : Disk c r) : (ofContinuousOn c r F hF) z = F ↑z

theorem NavierStokes.CauchyRestriction.derivativeCLM_apply_of_diffContOnCl {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (c : ℂ) {ρ σ : ℝ} (hgap : ρ < σ) (F : ℂ → E) (hF : DiffContOnCl ℂ F (Metric.ball c σ)) (z : Disk c ρ) : ((derivativeCLM c hgap) (ofContinuousOn c σ F ⋯)) z = deriv F ↑z

Agreement with the actual derivative under holomorphy in the open disk and continuity on its closure. No smoothness of the derivative is assumed.

theorem NavierStokes.CauchyRestriction.derivativeCLM_apply_of_differentiableOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (c : ℂ) {ρ σ : ℝ} (hgap : ρ < σ) (F : ℂ → E) (hF : DifferentiableOn ℂ F (Metric.closedBall c σ)) (z : Disk c ρ) : ((derivativeCLM c hgap) (ofContinuousOn c σ F ⋯)) z = deriv F ↑z

theorem NavierStokes.CauchyRestriction.restrict_derivativeCLM_of_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (c : ℂ) {r ρ σ : ℝ} (hr : r ≤ ρ) (hgap : ρ < σ) (f : C(Disk c σ, E)) (F : ℂ → E) (hF : DiffContOnCl ℂ F (Metric.ball c σ)) (hvalues : ∀ (w : Disk c σ), f w = F ↑w) : (restrictionCLM c hr) ((derivativeCLM c hgap) f) = (derivativeCLM c ⋯) f

On holomorphic data, further restriction of the derivative does not depend on which smaller target disk was used to construct the Cauchy integral.

theorem NavierStokes.CauchyRestriction.derivativeCLM_restrict_of_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (c : ℂ) {r ρ σ : ℝ} (hgap : r < ρ) (houter : ρ ≤ σ) (f : C(Disk c σ, E)) (F : ℂ → E) (hF : DiffContOnCl ℂ F (Metric.ball c σ)) (hvalues : ∀ (w : Disk c σ), f w = F ↑w) : (derivativeCLM c hgap) ((restrictionCLM c houter) f) = (derivativeCLM c ⋯) f

Restricting the source disk also gives the same derivative on common smaller disks, provided the source represents a holomorphic function.

theorem NavierStokes.CauchyRestriction.continuous_derivative_path {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {X : Type u_2} [TopologicalSpace X] (c : ℂ) {ρ σ : ℝ} (hgap : ρ < σ) {f : X → C(Disk c σ, E)} (hf : Continuous f) : Continuous fun (x : X) => (derivativeCLM c hgap) (f x)

theorem NavierStokes.CauchyRestriction.contDiff_derivative_path {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] (c : ℂ) {ρ σ : ℝ} (hgap : ρ < σ) {n : WithTop ℕ∞} {f : X → C(Disk c σ, E)} (hf : ContDiff ℝ n f) : ContDiff ℝ n fun (x : X) => (derivativeCLM c hgap) (f x)