Joint real smoothness of smooth families of holomorphic disk functions

A fixed-contour Cauchy formula realizes evaluation inside a disk as a smooth supremum-norm kernel paired with the supplied Banach-valued curve. This proves joint smoothness, rather than inferring it from separate smoothness.

@[reducible, inline]

abbrev NavierStokes.HolomorphicFamily.Angles : Type

Angles: an abbreviation for ↥(Icc (0 : ℝ) (2 * Real.pi)).

Equations

• NavierStokes.HolomorphicFamily.Angles = ↑(Set.Icc 0 (2 * Real.pi))

noncomputable def NavierStokes.HolomorphicFamily.angleExtend {E : Type u_1} [NormedAddCommGroup E] (f : C(Angles, E)) (θ : ℝ) : E

Continuous extension of an angle path, used only inside its integration interval.

Equations

• NavierStokes.HolomorphicFamily.angleExtend f θ = f (Set.projIcc 0 (2 * Real.pi) NavierStokes.HolomorphicFamily.angleExtend._proof_1 θ)

theorem NavierStokes.HolomorphicFamily.continuous_angleExtend {E : Type u_1} [NormedAddCommGroup E] (f : C(Angles, E)) : Continuous (angleExtend f)

theorem NavierStokes.HolomorphicFamily.angleExtend_coe {E : Type u_1} [NormedAddCommGroup E] (f : C(Angles, E)) (θ : Angles) : angleExtend f ↑θ = f θ

theorem NavierStokes.HolomorphicFamily.norm_angleIntegral_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : C(Angles, E)) : ‖∫ (θ : ℝ) in 0..2 * Real.pi, angleExtend f θ‖ ≤ 2 * Real.pi * ‖f‖

noncomputable def NavierStokes.HolomorphicFamily.angleIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] : C(Angles, E) →L[ℝ] E

Integration is a bounded real-linear map on continuous angle paths.

Equations

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

noncomputable def NavierStokes.HolomorphicFamily.circleInput (c : ℂ) {σ : ℝ} (hσ : 0 < σ) : C(Angles, CauchyRestriction.Disk c σ)

Sampling the outer circle as a continuous map into the closed disk.

Equations

• NavierStokes.HolomorphicFamily.circleInput c hσ = { toFun := fun (θ : NavierStokes.HolomorphicFamily.Angles) => ⟨circleMap c σ ↑θ, ⋯⟩, continuous_toFun := ⋯ }

noncomputable def NavierStokes.HolomorphicFamily.sampleCircle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ℂ) {σ : ℝ} (hσ : 0 < σ) : C(CauchyRestriction.Disk c σ, E) →L[ℝ] C(Angles, E)

Circle sampling has operator norm at most one.

Equations

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

noncomputable def NavierStokes.HolomorphicFamily.multiplyPaths {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (k : C(Angles, ℂ)) (v : C(Angles, E)) : C(Angles, E)

Pointwise complex multiplication of a scalar angle path and a vector path.

Equations

• NavierStokes.HolomorphicFamily.multiplyPaths k v = { toFun := fun (θ : NavierStokes.HolomorphicFamily.Angles) => k θ • v θ, continuous_toFun := ⋯ }

theorem NavierStokes.HolomorphicFamily.norm_multiplyPaths_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (k : C(Angles, ℂ)) (v : C(Angles, E)) : ‖multiplyPaths k v‖ ≤ ‖k‖ * ‖v‖

noncomputable def NavierStokes.HolomorphicFamily.multiplyPathsLinear {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] : C(Angles, ℂ) →ₗ[ℝ] C(Angles, E) →ₗ[ℝ] C(Angles, E)

Multiply paths linear, bundling toFun, toFun, map_add, map_smul and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.HolomorphicFamily.pathAction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] : C(Angles, ℂ) →L[ℝ] C(Angles, E) →L[ℝ] C(Angles, E)

A concrete bounded bilinear pairing of continuous contour paths.

Equations

• NavierStokes.HolomorphicFamily.pathAction = NavierStokes.HolomorphicFamily.multiplyPathsLinear.mkContinuous₂ 1 ⋯

noncomputable def NavierStokes.HolomorphicFamily.kernel (c : ℂ) (σ : ℝ) (p : ℂ × ℝ) : ℂ

The fixed-circle Cauchy kernel, including the circle's tangent factor.

Equations

• NavierStokes.HolomorphicFamily.kernel c σ p = circleMap 0 σ p.2 * Complex.I * (circleMap c σ p.2 - p.1)⁻¹

theorem NavierStokes.HolomorphicFamily.contDiffOn_kernel (c : ℂ) (σ : ℝ) : ContDiffOn ℝ (↑⊤) (kernel c σ) (Metric.ball c σ ×ˢ Set.univ)

noncomputable def NavierStokes.HolomorphicFamily.kernelPath (c : ℂ) (σ : ℝ) : ℂ → C(Angles, ℂ)

The Cauchy kernel is smooth as a supremum-norm continuous path.

Equations

• NavierStokes.HolomorphicFamily.kernelPath c σ = NavierStokes.CompactSmoothFamily.family (Set.Icc 0 (2 * Real.pi)) (NavierStokes.HolomorphicFamily.kernel c σ)

theorem NavierStokes.HolomorphicFamily.contDiffOn_kernelPath (c : ℂ) (σ : ℝ) : ContDiffOn ℝ (↑⊤) (kernelPath c σ) (Metric.ball c σ)

theorem NavierStokes.HolomorphicFamily.kernelPath_apply (c : ℂ) (σ : ℝ) {z : ℂ} (hz : z ∈ Metric.ball c σ) (θ : Angles) : (kernelPath c σ z) θ = circleMap 0 σ ↑θ * Complex.I * (circleMap c σ ↑θ - z)⁻¹

noncomputable def NavierStokes.HolomorphicFamily.cauchyValue {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ℂ) {σ : ℝ} (hσ : 0 < σ) (V : ℝ → C(CauchyRestriction.Disk c σ, E)) (p : ℝ × ℂ) : E

Fixed-contour evaluation, defined for every continuous outer-disk input.

Equations

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

theorem NavierStokes.HolomorphicFamily.contDiffOn_cauchyValue {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ℂ) {σ : ℝ} (hσ : 0 < σ) {S : Set ℝ} (V : ℝ → C(CauchyRestriction.Disk c σ, E)) (hV : ContDiffOn ℝ (↑⊤) V S) : ContDiffOn ℝ (↑⊤) (cauchyValue c hσ V) (S ×ˢ Metric.ball c σ)

Joint smoothness of the actual Cauchy integral follows from bounded bilinearity and supremum-norm smoothness of its two contour inputs.

theorem NavierStokes.HolomorphicFamily.diffContOnCl_of_values {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ℂ) {σ : ℝ} (v : C(CauchyRestriction.Disk c σ, E)) (F : ℂ → E) (hF : DifferentiableOn ℂ F (Metric.ball c σ)) (hvalues : ∀ (z : CauchyRestriction.Disk c σ), v z = F ↑z) : DiffContOnCl ℂ F (Metric.ball c σ)

Continuous disk data supplies the boundary-continuity part of the Cauchy formula.

theorem NavierStokes.HolomorphicFamily.cauchyValue_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (c : ℂ) {σ : ℝ} (hσ : 0 < σ) (V : ℝ → C(CauchyRestriction.Disk c σ, E)) (F : ℝ → ℂ → E) {r : ℝ} (hF : DifferentiableOn ℂ (F r) (Metric.ball c σ)) (hvalues : ∀ (z : CauchyRestriction.Disk c σ), (V r) z = F r ↑z) {z : ℂ} (hz : z ∈ Metric.ball c σ) : cauchyValue c hσ V (r, z) = F r z

The jointly smooth Cauchy expression agrees with every holomorphic slice represented by the given continuous disk input.

theorem NavierStokes.HolomorphicFamily.contDiffOn_of_disk_family {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (c : ℂ) {σ : ℝ} (hσ : 0 < σ) {S : Set ℝ} (V : ℝ → C(CauchyRestriction.Disk c σ, E)) (F : ℝ → ℂ → E) (hV : ContDiffOn ℝ (↑⊤) V S) (hF : ∀ r ∈ S, DifferentiableOn ℂ (F r) (Metric.ball c σ)) (hvalues : ∀ r ∈ S, ∀ (z : CauchyRestriction.Disk c σ), (V r) z = F r ↑z) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => F p.1 p.2) (S ×ˢ Metric.ball c σ)

A genuine smooth Banach-valued disk family of holomorphic slices is jointly real smooth throughout the open disk.

theorem NavierStokes.HolomorphicFamily.contDiffOn_of_disk_family_smaller {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (c : ℂ) {ρ σ : ℝ} (hσ : 0 < σ) (hgap : ρ < σ) {S : Set ℝ} (V : ℝ → C(CauchyRestriction.Disk c σ, E)) (F : ℝ → ℂ → E) (hV : ContDiffOn ℝ (↑⊤) V S) (hF : ∀ r ∈ S, DifferentiableOn ℂ (F r) (Metric.ball c σ)) (hvalues : ∀ r ∈ S, ∀ (z : CauchyRestriction.Disk c σ), (V r) z = F r ↑z) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => F p.1 p.2) (S ×ˢ Metric.ball c ρ)

The smaller-disk form used by the Volterra regularity construction.

noncomputable def NavierStokes.HolomorphicFamily.jointDerivative {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (a b : E) : ℝ × ℂ →L[ℝ] E

Real-linear joint derivative: a real radial increment and a complex disk increment act on the two actual partial derivatives.

Equations

• NavierStokes.HolomorphicFamily.jointDerivative a b = (ContinuousLinearMap.smulRight 1 a).coprod (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 b))

@[simp]

theorem NavierStokes.HolomorphicFamily.jointDerivative_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (a b : E) (v : ℝ × ℂ) : (jointDerivative a b) v = v.1 • a + v.2 • b

theorem NavierStokes.HolomorphicFamily.hasDerivAt_parameter {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ℂ) {σ : ℝ} {S : Set ℝ} (hS : IsOpen S) (V : ℝ → C(CauchyRestriction.Disk c σ, E)) (F : ℝ → ℂ → E) (hV : ContDiffOn ℝ (↑⊤) V S) (hvalues : ∀ r ∈ S, ∀ (z : CauchyRestriction.Disk c σ), (V r) z = F r ↑z) {r : ℝ} (hr : r ∈ S) (z : CauchyRestriction.Disk c σ) : HasDerivAt (fun (s : ℝ) => F s ↑z) ((deriv V r) z) r

The radial partial derivative is obtained by evaluating the genuine supremum-norm derivative of the supplied disk curve.

theorem NavierStokes.HolomorphicFamily.hasDerivAt_complex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (c : ℂ) {ρ σ : ℝ} (hgap : ρ < σ) (v : C(CauchyRestriction.Disk c σ, E)) (F : ℂ → E) (hF : DifferentiableOn ℂ F (Metric.ball c σ)) (hvalues : ∀ (z : CauchyRestriction.Disk c σ), v z = F ↑z) (z : CauchyRestriction.Disk c ρ) : HasDerivAt F (((CauchyRestriction.derivativeCLM c hgap) v) z) ↑z

CauchyRestriction's bounded operator is the actual complex partial.

theorem NavierStokes.HolomorphicFamily.hasFDerivAt_joint {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (c : ℂ) {ρ σ : ℝ} (hσ : 0 < σ) (hgap : ρ < σ) {S : Set ℝ} (hS : IsOpen S) (V : ℝ → C(CauchyRestriction.Disk c σ, E)) (F : ℝ → ℂ → E) (hV : ContDiffOn ℝ (↑⊤) V S) (hF : ∀ r ∈ S, DifferentiableOn ℂ (F r) (Metric.ball c σ)) (hvalues : ∀ r ∈ S, ∀ (z : CauchyRestriction.Disk c σ), (V r) z = F r ↑z) {r : ℝ} (hr : r ∈ S) (z : CauchyRestriction.Disk c ρ) : HasFDerivAt (fun (p : ℝ × ℂ) => F p.1 p.2) (jointDerivative ((deriv V r) ⟨↑z, ⋯⟩) (((CauchyRestriction.derivativeCLM c hgap) (V r)) z)) (r, ↑z)

The actual joint Fréchet derivative combines the supremum-norm radial derivative with the bounded Cauchy differentiation operator.

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

The Cauchy partial has the expected inverse-gap bound.

theorem NavierStokes.HolomorphicFamily.differentiableAt_of_evaluations {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {K : Type u_2} [TopologicalSpace K] [CompactSpace K] (G : ℂ → C(K, E)) {z : ℂ} (hG : DifferentiableAt ℝ G z) (heval : ∀ (x : K), DifferentiableAt ℂ (fun (w : ℂ) => (G w) x) z) : DifferentiableAt ℂ G z

Real differentiability into a compact-function Banach space upgrades to complex differentiability when every evaluation has a complex derivative. The complex linearity is proved by the separating evaluation maps.

theorem NavierStokes.HolomorphicFamily.differentiableOn_family_of_joint {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] (K : Set ℝ) [CompactSpace ↑K] (U : Set ℂ) (V : Set ℝ) (hU : IsOpen U) (hV : IsOpen V) (hKV : K ⊆ V) (G : ℂ × ℝ → B) (hG : ContDiffOn ℝ (↑⊤) G (U ×ˢ V)) (hhol : ∀ r ∈ K, DifferentiableOn ℂ (fun (z : ℂ) => G (z, r)) U) : DifferentiableOn ℂ (CompactSmoothFamily.family K G) U

Joint real smoothness near a compact radial set and holomorphic parameter slices give genuine complex differentiability of the compact-valued family. This is the input bridge for compact-family Volterra operators.