Radial smoothness for the actual regular Volterra integral

The radial integral gains one real derivative, including at the origin. The intended bootstrap uses bounded parameter-derivative operators between nested complex disks; no analyticity in the radial variable is assumed.

The radial domain is an open symmetric interval. In particular these results do not identify the clamped extension of a positive path with a smooth extension across zero.

@[reducible, inline]

abbrev NavierStokes.VolterraRegularity.radialDomain (R : ℝ) : Set ℝ

Radial domain: an abbreviation for Metric.ball 0 R.

Equations

• NavierStokes.VolterraRegularity.radialDomain R = Metric.ball 0 R

theorem NavierStokes.VolterraRegularity.scaled_mem_radialDomain {R r t : ℝ} (hr : r ∈ radialDomain R) (ht : t ∈ Set.Icc 0 1) : t * r ∈ radialDomain R

theorem NavierStokes.VolterraRegularity.weightedMean_continuousOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℕ) {R : ℝ} {f : ℝ → E} (hf : ContinuousOn f (radialDomain R)) : ContinuousOn (NilpotentVolterra.weightedMean c f) (radialDomain R)

Continuity of the actual weighted integral needs continuity only on the radial domain. The integration variable is clamped solely outside [0,1] to apply the global parameter-integral continuity theorem.

theorem NavierStokes.VolterraRegularity.weightedMean_eq_of_eqOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℕ) {R : ℝ} {f g : ℝ → E} (hfg : Set.EqOn f g (radialDomain R)) {r : ℝ} (hr : r ∈ radialDomain R) : NilpotentVolterra.weightedMean c f r = NilpotentVolterra.weightedMean c g r

theorem NavierStokes.VolterraRegularity.regularPrimitive_eq_of_eqOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℕ) {R : ℝ} {f g : ℝ → E} (hfg : Set.EqOn f g (radialDomain R)) {r : ℝ} (hr : r ∈ radialDomain R) : NilpotentVolterra.regularPrimitive c f r = NilpotentVolterra.regularPrimitive c g r

theorem NavierStokes.VolterraRegularity.regularPrimitive_hasDerivAt_on {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (c : ℕ) {R : ℝ} {f : ℝ → E} (hf : ContinuousOn f (radialDomain R)) {r : ℝ} (hr : r ∈ radialDomain R) : HasDerivAt (NilpotentVolterra.regularPrimitive c f) (f r - ↑c • NilpotentVolterra.weightedMean c f r) r

The nonsingular first derivative formula is local on the radial domain. Its proof uses a continuous extension only to invoke the already established integral identity; the claimed function remains the original integral.

theorem NavierStokes.VolterraRegularity.weightedMean_hasDerivAt_on {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℕ) {R : ℝ} {f : ℝ → E} (hf : ContinuousOn f (radialDomain R)) (hdf : DifferentiableOn ℝ f (radialDomain R)) (hf' : ContinuousOn (deriv f) (radialDomain R)) {r : ℝ} (hr : r ∈ radialDomain R) : HasDerivAt (NilpotentVolterra.weightedMean c f) (NilpotentVolterra.weightedMean (c + 1) (deriv f) r) r

Differentiation under the actual weighted integral. A compact radial subinterval supplies the integrable domination, so no global derivative bound or radial analyticity is needed.

theorem NavierStokes.VolterraRegularity.weightedMean_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (n c : ℕ) {R : ℝ} {f : ℝ → E} (hf : ContDiffOn ℝ (↑n) f (radialDomain R)) : ContDiffOn ℝ (↑n) (NilpotentVolterra.weightedMean c f) (radialDomain R)

The weighted mean preserves every finite radial differentiability order.

theorem NavierStokes.VolterraRegularity.regularPrimitive_contDiffOn_succ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (n c : ℕ) {R : ℝ} {f : ℝ → E} (hf : ContDiffOn ℝ (↑n) f (radialDomain R)) : ContDiffOn ℝ (↑(n + 1)) (NilpotentVolterra.regularPrimitive c f) (radialDomain R)

The regular Volterra integral gains one full real derivative. The domain contains zero, so this includes the formerly singular endpoint.

theorem NavierStokes.VolterraRegularity.regularPrimitive_contDiffOn_infty {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (c : ℕ) {R : ℝ} {f : ℝ → E} (hf : ContDiffOn ℝ (↑⊤) f (radialDomain R)) : ContDiffOn ℝ (↑⊤) (NilpotentVolterra.regularPrimitive c f) (radialDomain R)

noncomputable def NavierStokes.VolterraRegularity.diagonalRegularPrimitive {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ι → ℕ) (f : ℝ → ι → E) : ℝ → ι → E

The actual coordinatewise regular inverse, for arbitrary nonnegative integer singular exponents. In the six-component system these are (0,0,2,0,3,1).

Equations

• NavierStokes.VolterraRegularity.diagonalRegularPrimitive c f r i = NavierStokes.NilpotentVolterra.regularPrimitive (c i) (fun (s : ℝ) => f s i) r

theorem NavierStokes.VolterraRegularity.diagonalRegularPrimitive_contDiffOn_succ {ι : Type u_1} {E : Type u_2} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (n : ℕ) (c : ι → ℕ) {R : ℝ} {f : ℝ → ι → E} (hf : ContDiffOn ℝ (↑n) f (radialDomain R)) : ContDiffOn ℝ (↑(n + 1)) (diagonalRegularPrimitive c f) (radialDomain R)

theorem NavierStokes.VolterraRegularity.scale_contDiffOn {ι : Type u_1} [Fintype ι] {B : ℕ → Type u} [(j : ℕ) → NormedAddCommGroup (B j)] [(j : ℕ) → NormedSpace ℝ (B j)] [∀ (j : ℕ), CompleteSpace (B j)] (c : ι → ℕ) {R : ℝ} (W f : (j : ℕ) → ℝ → ι → B j) (A₀ : (j : ℕ) → ℝ → (ι → B j) →L[ℝ] ι → B j) (A₁ : (j : ℕ) → ℝ → (ι → B (j + 1)) →L[ℝ] ι → B j) (hW : ∀ (j : ℕ), ContinuousOn (W j) (radialDomain R)) (hf : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (f j) (radialDomain R)) (hA₀ : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A₀ j) (radialDomain R)) (hA₁ : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A₁ j) (radialDomain R)) (heq : ∀ (j : ℕ), Set.EqOn (W j) (diagonalRegularPrimitive c fun (r : ℝ) => f j r + (A₀ j r) (W j r) + (A₁ j r) (W (j + 1) r)) (radialDomain R)) (j : ℕ) : ContDiffOn ℝ (↑⊤) (W j) (radialDomain R)

A genuine radial bootstrap on a sequence of Banach spaces. The next level is the larger parameter disk; its bounded Cauchy derivative is folded into A₁. The only initial regularity imposed on the solution is continuity.

theorem NavierStokes.VolterraRegularity.algebraScale_contDiffOn {ι : Type u_1} [Fintype ι] {B : ℕ → Type u} [(j : ℕ) → NormedRing (B j)] [(j : ℕ) → NormedAlgebra ℝ (B j)] [∀ (j : ℕ), CompleteSpace (B j)] (c : ι → ℕ) {R : ℝ} (W f : (j : ℕ) → ℝ → ι → B j) (a₀ a₁ : (j : ℕ) → ℝ → ι → ι → B j) (D : (j : ℕ) → B (j + 1) →L[ℝ] B j) (hW : ∀ (j : ℕ) (i : ι), ContinuousOn (fun (r : ℝ) => W j r i) (radialDomain R)) (hf : ∀ (j : ℕ) (i : ι), ContDiffOn ℝ (↑⊤) (fun (r : ℝ) => f j r i) (radialDomain R)) (ha₀ : ∀ (j : ℕ) (i k : ι), ContDiffOn ℝ (↑⊤) (fun (r : ℝ) => a₀ j r i k) (radialDomain R)) (ha₁ : ∀ (j : ℕ) (i k : ι), ContDiffOn ℝ (↑⊤) (fun (r : ℝ) => a₁ j r i k) (radialDomain R)) (heq : ∀ (j : ℕ) (i : ι), Set.EqOn (fun (r : ℝ) => W j r i) (NilpotentVolterra.regularPrimitive (c i) fun (r : ℝ) => f j r i + ∑ k : ι, a₀ j r i k * W j r k + ∑ k : ι, a₁ j r i k * (D j) (W (j + 1) r k)) (radialDomain R)) (j : ℕ) (i : ι) : ContDiffOn ℝ (↑⊤) (fun (r : ℝ) => W j r i) (radialDomain R)

Entrywise version of the scale bootstrap, convenient for matrices of continuous functions on compact parameter disks.

theorem NavierStokes.VolterraRegularity.regularPrimitive_evaluate {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (c : ℕ) {R : ℝ} {f : ℝ → C(K, E)} (hf : ContinuousOn f (radialDomain R)) {r : ℝ} (hr : r ∈ radialDomain R) (z : K) : (NilpotentVolterra.regularPrimitive c f r) z = NilpotentVolterra.regularPrimitive c (fun (s : ℝ) => (f s) z) r

Evaluation commutes with the actual radial integral when its source is continuous on the radial domain.

theorem NavierStokes.VolterraRegularity.radialDomain_subset_Icc (R : ℝ) : radialDomain R ⊆ Set.Icc (-R) R

noncomputable def NavierStokes.VolterraRegularity.radiusProjection (R : ℝ) (hR : 0 ≤ R) (r : ℝ) : ↑(Set.Icc (-R) R)

Continuous global parameterization of the trace. Only its restriction to the open radial domain will be asserted to be smooth.

Equations

• NavierStokes.VolterraRegularity.radiusProjection R hR r = Set.projIcc (-R) R ⋯ r

theorem NavierStokes.VolterraRegularity.radiusProjection_continuous (R : ℝ) (hR : 0 ≤ R) : Continuous (radiusProjection R hR)

theorem NavierStokes.VolterraRegularity.radiusProjection_eq (R : ℝ) (hR : 0 ≤ R) {r : ℝ} (hr : r ∈ Set.Icc (-R) R) : ↑(radiusProjection R hR r) = r

noncomputable def NavierStokes.VolterraRegularity.fieldDiskCurve (R : ℝ) (hR : 0 ≤ R) {U : Set ℂ} (W : VolterraAnalyticBounds.Field) (hW : ContinuousOn (fun (p : ℝ × ℂ) => W p.1 p.2) (Set.Icc (-R) R ×ˢ U)) (center : ℂ) (ρ : ℝ) (hDisk : Metric.closedBall center ρ ⊆ U) (r : ℝ) (i : Fin 6) : C(CauchyRestriction.Disk center ρ, ℂ)

A continuous parameter-disk curve formed from the actual field. The projection only defines values outside the radial interval; it is the identity everywhere used in the regularity theorem.

Equations

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

theorem NavierStokes.VolterraRegularity.fieldDiskCurve_continuous (R : ℝ) (hR : 0 ≤ R) {U : Set ℂ} (W : VolterraAnalyticBounds.Field) (hW : ContinuousOn (fun (p : ℝ × ℂ) => W p.1 p.2) (Set.Icc (-R) R ×ˢ U)) (center : ℂ) (ρ : ℝ) (hDisk : Metric.closedBall center ρ ⊆ U) (i : Fin 6) : Continuous fun (r : ℝ) => fieldDiskCurve R hR W hW center ρ hDisk r i

theorem NavierStokes.VolterraRegularity.fieldDiskCurve_apply (R : ℝ) (hR : 0 ≤ R) {U : Set ℂ} (W : VolterraAnalyticBounds.Field) (hW : ContinuousOn (fun (p : ℝ × ℂ) => W p.1 p.2) (Set.Icc (-R) R ×ˢ U)) (center : ℂ) (ρ : ℝ) (hDisk : Metric.closedBall center ρ ⊆ U) {r : ℝ} (hr : r ∈ Set.Icc (-R) R) (i : Fin 6) (z : CauchyRestriction.Disk center ρ) : (fieldDiskCurve R hR W hW center ρ hDisk r i) z = W r (↑z) i

theorem NavierStokes.VolterraRegularity.fieldDiskCurve_radial_contDiffOn (R : ℝ) (hR : 0 ≤ R) {U : Set ℂ} (W : VolterraAnalyticBounds.Field) (hW : ContinuousOn (fun (p : ℝ × ℂ) => W p.1 p.2) (Set.Icc (-R) R ×ˢ U)) (center : ℂ) (ρ : ℝ) (hDisk : Metric.closedBall center ρ ⊆ U) (i : Fin 6) (n : WithTop ℕ∞) (hs : ContDiffOn ℝ n (fun (r : ℝ) => fieldDiskCurve R hR W hW center ρ hDisk r i) (radialDomain R)) (z : CauchyRestriction.Disk center ρ) : ContDiffOn ℝ n (fun (r : ℝ) => W r (↑z) i) (radialDomain R)

Smoothness of the disk-valued curve implies actual scalar radial smoothness, by bounded evaluation.

theorem NavierStokes.VolterraRegularity.symmetric_solution_disk_curves_contDiffOn {R : ℝ} (hR : 0 ≤ R) {U : Set ℂ} {A₀ A₁ : VolterraAnalyticBounds.Coeff} {f W : VolterraAnalyticBounds.Field} (hW : VolterraParity.IsSymmetricIntegralSolution R U A₀ A₁ f W) (center : ℂ) (ρ : ℕ → ℝ) (hρ : ∀ (j : ℕ), ρ j < ρ (j + 1)) (hDisk : ∀ (j : ℕ), Metric.closedBall center (ρ j) ⊆ U) (b : (j : ℕ) → ℝ → Fin 6 → C(CauchyRestriction.Disk center (ρ j), ℂ)) (a₀ a₁ : (j : ℕ) → ℝ → Fin 6 → Fin 6 → C(CauchyRestriction.Disk center (ρ j), ℂ)) (hb : ∀ (j : ℕ) (i : Fin 6), ContDiffOn ℝ (↑⊤) (fun (r : ℝ) => b j r i) (radialDomain R)) (ha₀ : ∀ (j : ℕ) (i k : Fin 6), ContDiffOn ℝ (↑⊤) (fun (r : ℝ) => a₀ j r i k) (radialDomain R)) (ha₁ : ∀ (j : ℕ) (i k : Fin 6), ContDiffOn ℝ (↑⊤) (fun (r : ℝ) => a₁ j r i k) (radialDomain R)) (hbval : ∀ (j : ℕ), ∀ r ∈ radialDomain R, ∀ (i : Fin 6) (z : CauchyRestriction.Disk center (ρ j)), (b j r i) z = f r (↑z) i) (ha₀val : ∀ (j : ℕ), ∀ r ∈ radialDomain R, ∀ (i k : Fin 6) (z : CauchyRestriction.Disk center (ρ j)), (a₀ j r i k) z = A₀ r (↑z) i k) (ha₁val : ∀ (j : ℕ), ∀ r ∈ radialDomain R, ∀ (i k : Fin 6) (z : CauchyRestriction.Disk center (ρ j)), (a₁ j r i k) z = A₁ r (↑z) i k) (j : ℕ) (i : Fin 6) : ContDiffOn ℝ (↑⊤) (fun (r : ℝ) => fieldDiskCurve R hR W ⋯ center (ρ j) ⋯ r i) (radialDomain R)

Actual radial regularity of a symmetric integral solution. The smooth inputs are disk-valued representations of the coefficients and forcing; their value identities are explicit. Continuity and holomorphy of the constructed solution come solely from IsSymmetricIntegralSolution.

The radii increase with the level. Each induction step spends one disk gap through the concrete bounded Cauchy operator and gains one radial derivative through the actual regular Volterra integral.

noncomputable def NavierStokes.VolterraRegularity.cauchyJetCurve {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (center : ℂ) (ρ : ℕ → ℝ) (hρ : ∀ (j : ℕ), ρ j < ρ (j + 1)) (V : (j : ℕ) → ℝ → C(CauchyRestriction.Disk center (ρ j), E)) : ℕ → (j : ℕ) → ℝ → C(CauchyRestriction.Disk center (ρ j), E)

Iterated Cauchy differentiation spends one disk gap at each step.

Equations

• One or more equations did not get rendered due to their size.
• NavierStokes.VolterraRegularity.cauchyJetCurve center ρ hρ V 0 x✝¹ x✝ = V x✝¹ x✝

theorem NavierStokes.VolterraRegularity.cauchyJetCurve_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (center : ℂ) (ρ : ℕ → ℝ) (hρ : ∀ (j : ℕ), ρ j < ρ (j + 1)) (V : (j : ℕ) → ℝ → C(CauchyRestriction.Disk center (ρ j), E)) {S : Set ℝ} {n : WithTop ℕ∞} (hV : ∀ (j : ℕ), ContDiffOn ℝ n (V j) S) (k j : ℕ) : ContDiffOn ℝ n (cauchyJetCurve center ρ hρ V k j) S

theorem NavierStokes.VolterraRegularity.holomorphic_iteratedDeriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {U : Set ℂ} (hU : IsOpen U) {F : ℂ → E} (hF : DifferentiableOn ℂ F U) (k : ℕ) : DifferentiableOn ℂ (iteratedDeriv k F) U

theorem NavierStokes.VolterraRegularity.cauchyJetCurve_apply_of_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (center : ℂ) (ρ : ℕ → ℝ) (hρ : ∀ (j : ℕ), ρ j < ρ (j + 1)) (V : (j : ℕ) → ℝ → C(CauchyRestriction.Disk center (ρ j), E)) {S : Set ℝ} {U : Set ℂ} (hU : IsOpen U) (hDisk : ∀ (j : ℕ), Metric.closedBall center (ρ j) ⊆ U) (F : ℝ → ℂ → E) (hF : ∀ r ∈ S, DifferentiableOn ℂ (F r) U) (hV : ∀ (j : ℕ), ∀ r ∈ S, ∀ (z : CauchyRestriction.Disk center (ρ j)), (V j r) z = F r ↑z) (k j : ℕ) (r : ℝ) : r ∈ S → ∀ (z : CauchyRestriction.Disk center (ρ j)), (cauchyJetCurve center ρ hρ V k j r) z = iteratedDeriv k (F r) ↑z

On holomorphic data the iterated bounded operators are the actual iterated complex derivatives, at every point of the smaller closed disk.

theorem NavierStokes.VolterraRegularity.parameterJets_radial_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (center : ℂ) (ρ : ℕ → ℝ) (hρ : ∀ (j : ℕ), ρ j < ρ (j + 1)) (V : (j : ℕ) → ℝ → C(CauchyRestriction.Disk center (ρ j), E)) {S : Set ℝ} {U : Set ℂ} (hU : IsOpen U) (hDisk : ∀ (j : ℕ), Metric.closedBall center (ρ j) ⊆ U) (F : ℝ → ℂ → E) (hF : ∀ r ∈ S, DifferentiableOn ℂ (F r) U) (hV : ∀ (j : ℕ), ∀ r ∈ S, ∀ (z : CauchyRestriction.Disk center (ρ j)), (V j r) z = F r ↑z) (hs : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (V j) S) (k j : ℕ) (z : CauchyRestriction.Disk center (ρ j)) : ContDiffOn ℝ (↑⊤) (fun (r : ℝ) => iteratedDeriv k (F r) ↑z) S

All parameter jets are smooth functions of the real radial variable. The assertion follows from bounded operators and does not posit mixed regularity of the original field.

theorem NavierStokes.VolterraRegularity.real_iteratedDeriv_contDiffOn {G : Type u_2} [NormedAddCommGroup G] [NormedSpace ℝ G] {S : Set ℝ} (hS : IsOpen S) {f : ℝ → G} (hf : ContDiffOn ℝ (↑⊤) f S) (n : ℕ) : ContDiffOn ℝ (↑⊤) (iteratedDeriv n f) S

theorem NavierStokes.VolterraRegularity.iteratedDeriv_evaluate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {K : Type u_2} [TopologicalSpace K] [CompactSpace K] {S : Set ℝ} (hS : IsOpen S) {f : ℝ → C(K, E)} (hf : ContDiffOn ℝ (↑⊤) f S) {r : ℝ} (hr : r ∈ S) (n : ℕ) (z : K) : (iteratedDeriv n f r) z = iteratedDeriv n (fun (s : ℝ) => (f s) z) r

Evaluation of a smooth compact-function curve commutes with every fixed radial derivative.

theorem NavierStokes.VolterraRegularity.parameterJets_uniform_mixed_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (center : ℂ) (ρ : ℕ → ℝ) (hρ : ∀ (j : ℕ), ρ j < ρ (j + 1)) (V : (j : ℕ) → ℝ → C(CauchyRestriction.Disk center (ρ j), E)) {S : Set ℝ} (hS : IsOpen S) {U : Set ℂ} (hU : IsOpen U) (hDisk : ∀ (j : ℕ), Metric.closedBall center (ρ j) ⊆ U) (F : ℝ → ℂ → E) (hF : ∀ r ∈ S, DifferentiableOn ℂ (F r) U) (hV : ∀ (j : ℕ), ∀ r ∈ S, ∀ (z : CauchyRestriction.Disk center (ρ j)), (V j r) z = F r ↑z) (hs : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (V j) S) {K : Set ℝ} (hK : IsCompact K) (hKS : K ⊆ S) (n k j : ℕ) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ r ∈ K, ∀ (z : CauchyRestriction.Disk center (ρ j)), ‖iteratedDeriv n (fun (s : ℝ) => iteratedDeriv k (F s) ↑z) r‖ ≤ B

Compact radial subintervals have uniform bounds for each fixed mixed derivative on the full inner parameter disk. Constants may depend on both derivative orders; no radial analyticity estimate is asserted.

structure NavierStokes.VolterraRegularity.SmoothCoefficientData (R : ℝ) (U : Set ℂ) (A₀ A₁ : VolterraAnalyticBounds.Coeff) (f : VolterraAnalyticBounds.Field) : Prop

Regularity assumptions on the input coefficients only. The forcing and all matrix entries are jointly smooth in the real radial variable and the two real coordinates of the complex parameter.

• forcing (i : Fin 6) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => f p.1 p.2 i) (radialDomain R ×ˢ U)
• zeroth (i k : Fin 6) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => A₀ p.1 p.2 i k) (radialDomain R ×ˢ U)
• first (i k : Fin 6) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => A₁ p.1 p.2 i k) (radialDomain R ×ˢ U)

theorem NavierStokes.VolterraRegularity.symmetric_solution_disk_curves_of_smooth_coefficients {R : ℝ} (hR : 0 ≤ R) {U : Set ℂ} (hU : IsOpen U) {A₀ A₁ : VolterraAnalyticBounds.Coeff} {f W : VolterraAnalyticBounds.Field} (hW : VolterraParity.IsSymmetricIntegralSolution R U A₀ A₁ f W) (hdata : SmoothCoefficientData R U A₀ A₁ f) (center : ℂ) (ρ : ℕ → ℝ) (hρ : ∀ (j : ℕ), ρ j < ρ (j + 1)) (hDisk : ∀ (j : ℕ), Metric.closedBall center (ρ j) ⊆ U) (j : ℕ) (i : Fin 6) : ContDiffOn ℝ (↑⊤) (fun (r : ℝ) => fieldDiskCurve R hR W ⋯ center (ρ j) ⋯ r i) (radialDomain R)

The smooth disk-valued inputs required by the bootstrap are constructed from the actual jointly smooth coefficient entries.

theorem NavierStokes.VolterraRegularity.symmetric_solution_parameterJets_radial_contDiffOn {R : ℝ} (hR : 0 ≤ R) {U : Set ℂ} (hU : IsOpen U) {A₀ A₁ : VolterraAnalyticBounds.Coeff} {f W : VolterraAnalyticBounds.Field} (hW : VolterraParity.IsSymmetricIntegralSolution R U A₀ A₁ f W) (hdata : SmoothCoefficientData R U A₀ A₁ f) (center : ℂ) (ρ : ℕ → ℝ) (hρ : ∀ (j : ℕ), ρ j < ρ (j + 1)) (hDisk : ∀ (j : ℕ), Metric.closedBall center (ρ j) ⊆ U) (k j : ℕ) (i : Fin 6) (z : CauchyRestriction.Disk center (ρ j)) : ContDiffOn ℝ (↑⊤) (fun (r : ℝ) => iteratedDeriv k (fun (w : ℂ) => W r w i) ↑z) (radialDomain R)

Every fixed complex parameter derivative of the actual symmetric solution is real smooth through the radial origin.

noncomputable def NavierStokes.VolterraRegularity.interiorRadii (δ : ℝ) (j : ℕ) : ℝ

An explicit sequence of interior radii, with infinitely many positive gaps before the boundary of the available parameter neighborhood.

Equations

• NavierStokes.VolterraRegularity.interiorRadii δ j = δ - δ / (↑j + 2)

theorem NavierStokes.VolterraRegularity.interiorRadii_pos {δ : ℝ} (hδ : 0 < δ) (j : ℕ) : 0 < interiorRadii δ j

theorem NavierStokes.VolterraRegularity.interiorRadii_lt {δ : ℝ} (hδ : 0 < δ) (j : ℕ) : interiorRadii δ j < δ

theorem NavierStokes.VolterraRegularity.interiorRadii_increasing {δ : ℝ} (hδ : 0 < δ) (j : ℕ) : interiorRadii δ j < interiorRadii δ (j + 1)

theorem NavierStokes.VolterraRegularity.interiorRadii_subset {δ : ℝ} (hδ : 0 < δ) (center : ℂ) {U : Set ℂ} (hball : Metric.ball center δ ⊆ U) (j : ℕ) : Metric.closedBall center (interiorRadii δ j) ⊆ U

theorem NavierStokes.VolterraRegularity.symmetric_solution_parameterJets_radial_contDiffOn_local {R : ℝ} (hR : 0 ≤ R) {U : Set ℂ} (hU : IsOpen U) {A₀ A₁ : VolterraAnalyticBounds.Coeff} {f W : VolterraAnalyticBounds.Field} (hW : VolterraParity.IsSymmetricIntegralSolution R U A₀ A₁ f W) (hdata : SmoothCoefficientData R U A₀ A₁ f) {z : ℂ} (hz : z ∈ U) (k : ℕ) (i : Fin 6) : ContDiffOn ℝ (↑⊤) (fun (r : ℝ) => iteratedDeriv k (fun (w : ℂ) => W r w i) z) (radialDomain R)

The nested disks can always be selected inside an open parameter domain. Thus every actual parameter jet is radially smooth at every parameter point, with no auxiliary disk-family hypothesis.

theorem NavierStokes.VolterraRegularity.symmetric_solution_mixed_contDiffOn {R : ℝ} (hR : 0 ≤ R) {U : Set ℂ} (hU : IsOpen U) {A₀ A₁ : VolterraAnalyticBounds.Coeff} {f W : VolterraAnalyticBounds.Field} (hW : VolterraParity.IsSymmetricIntegralSolution R U A₀ A₁ f W) (hdata : SmoothCoefficientData R U A₀ A₁ f) {z : ℂ} (hz : z ∈ U) (n k : ℕ) (i : Fin 6) : ContDiffOn ℝ (↑⊤) (iteratedDeriv n fun (r : ℝ) => iteratedDeriv k (fun (w : ℂ) => W r w i) z) (radialDomain R)

All fixed mixed derivatives of the constructed field exist smoothly through the real radial origin. The order of operations here is parameter differentiation followed by radial differentiation.

theorem NavierStokes.VolterraRegularity.symmetric_solution_mixed_contDiffAt_zero {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) {A₀ A₁ : VolterraAnalyticBounds.Coeff} {f W : VolterraAnalyticBounds.Field} (hW : VolterraParity.IsSymmetricIntegralSolution R U A₀ A₁ f W) (hdata : SmoothCoefficientData R U A₀ A₁ f) {z : ℂ} (hz : z ∈ U) (n k : ℕ) (i : Fin 6) : ContDiffAt ℝ (↑⊤) (iteratedDeriv n fun (r : ℝ) => iteratedDeriv k (fun (w : ℂ) => W r w i) z) 0

theorem NavierStokes.VolterraRegularity.symmetric_solution_radial_contDiffOn {R : ℝ} (hR : 0 ≤ R) {U : Set ℂ} (hU : IsOpen U) {A₀ A₁ : VolterraAnalyticBounds.Coeff} {f W : VolterraAnalyticBounds.Field} (hW : VolterraParity.IsSymmetricIntegralSolution R U A₀ A₁ f W) (hdata : SmoothCoefficientData R U A₀ A₁ f) {z : ℂ} (hz : z ∈ U) : ContDiffOn ℝ (↑⊤) (fun (r : ℝ) => W r z) (radialDomain R)

theorem NavierStokes.VolterraRegularity.symmetric_solution_uniform_mixed_bound {R : ℝ} (hR : 0 ≤ R) {U : Set ℂ} (hU : IsOpen U) {A₀ A₁ : VolterraAnalyticBounds.Coeff} {f W : VolterraAnalyticBounds.Field} (hW : VolterraParity.IsSymmetricIntegralSolution R U A₀ A₁ f W) (hdata : SmoothCoefficientData R U A₀ A₁ f) (center : ℂ) (ρ : ℕ → ℝ) (hρ : ∀ (j : ℕ), ρ j < ρ (j + 1)) (hDisk : ∀ (j : ℕ), Metric.closedBall center (ρ j) ⊆ U) {K : Set ℝ} (hK : IsCompact K) (hKR : K ⊆ radialDomain R) (n k j : ℕ) (i : Fin 6) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ r ∈ K, ∀ (z : CauchyRestriction.Disk center (ρ j)), ‖iteratedDeriv n (fun (s : ℝ) => iteratedDeriv k (fun (w : ℂ) => W s w i) ↑z) r‖ ≤ B

theorem NavierStokes.VolterraRegularity.symmetricSolution_mixed_contDiffOn {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → VolterraParity.SymmetricCoefficientPath R} {f : ℂ → VolterraParity.SymmetricPath R VolterraAnalyticBounds.Vec} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hf : DifferentiableOn ℂ f U) (hshape : VolterraAnalyticBounds.DerivativeShape (VolterraParity.symmetricRawCoefficient hR A₁)) (hdata : SmoothCoefficientData R U (VolterraParity.symmetricRawCoefficient hR A₀) (VolterraParity.symmetricRawCoefficient hR A₁) (VolterraParity.symmetricRawField hR f)) {z : ℂ} (hz : z ∈ U) (n k : ℕ) (i : Fin 6) : ContDiffOn ℝ (↑⊤) (iteratedDeriv n fun (r : ℝ) => iteratedDeriv k (fun (w : ℂ) => VolterraParity.symmetricSolution hR A₀ A₁ f r w i) z) (radialDomain R)

Direct specialization to the two-sided solution constructed from the convergent nilpotent Volterra series. No regularity of that output is an input to this theorem.

theorem NavierStokes.VolterraRegularity.symmetricSolution_mixed_contDiffAt_zero {R : ℝ} (hR : 0 < R) {A₀ A₁ : ℂ → VolterraParity.SymmetricCoefficientPath R} {f : ℂ → VolterraParity.SymmetricPath R VolterraAnalyticBounds.Vec} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hf : DifferentiableOn ℂ f U) (hshape : VolterraAnalyticBounds.DerivativeShape (VolterraParity.symmetricRawCoefficient ⋯ A₁)) (hdata : SmoothCoefficientData R U (VolterraParity.symmetricRawCoefficient ⋯ A₀) (VolterraParity.symmetricRawCoefficient ⋯ A₁) (VolterraParity.symmetricRawField ⋯ f)) {z : ℂ} (hz : z ∈ U) (n k : ℕ) (i : Fin 6) : ContDiffAt ℝ (↑⊤) (iteratedDeriv n fun (r : ℝ) => iteratedDeriv k (fun (w : ℂ) => VolterraParity.symmetricSolution ⋯ A₀ A₁ f r w i) z) 0