Local slow-order recursion from actual lower profiles

The source algebra consists of genuine smooth, even radial functions with holomorphic parameter dependence. No preconstructed all-order jet family is assumed.

Actual positive-order axis solutions

This module connects the sparse six-component Volterra construction to the explicit positive-order system, and to smooth profiles in the squared radius. All existence assertions are obtained from the actual convergent series.

@[instance_reducible]

noncomputable def NavierStokes.PositiveAxisExistence.instPositiveAxisExistence1 : NormedAddCommGroup (Matrix (Fin 6) (Fin 6) ℂ)

Cache the standard NormedAddCommGroup (Matrix (Fin 6) (Fin 6) ℂ) instance to shorten typeclass synthesis.

Equations

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

@[instance_reducible]

noncomputable def NavierStokes.PositiveAxisExistence.instPositiveAxisExistence2 : NormedSpace ℝ (Matrix (Fin 6) (Fin 6) ℂ)

Cache the standard NormedSpace ℝ (Matrix (Fin 6) (Fin 6) ℂ) instance to shorten typeclass synthesis.

Equations

• NavierStokes.PositiveAxisExistence.instPositiveAxisExistence2 = { toModule := Matrix.module, norm_smul_le := NavierStokes.PositiveAxisExistence.instPositiveAxisExistence2._proof_1 }

@[instance_reducible]

noncomputable def NavierStokes.PositiveAxisExistence.instPositiveAxisExistence3 : NormedSpace ℂ (Matrix (Fin 6) (Fin 6) ℂ)

Cache the standard NormedSpace ℂ (Matrix (Fin 6) (Fin 6) ℂ) instance to shorten typeclass synthesis.

Equations

• NavierStokes.PositiveAxisExistence.instPositiveAxisExistence3 = { toModule := Matrix.module, norm_smul_le := NavierStokes.PositiveAxisExistence.instPositiveAxisExistence3._proof_1 }

theorem NavierStokes.PositiveAxisExistence.equationRHS_radial_continuous {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 : VolterraRegularity.SmoothCoefficientData R U A₀ A₁ f) {z : ℂ} (hz : z ∈ U) (i : Fin 6) : ContinuousOn (fun (r : ℝ) => NilpotentVolterra.equationRHS A₀ A₁ f W r z i) (VolterraRegularity.radialDomain R)

The right side of the actual integral equation is radially continuous; the parameter derivative is supplied by the proved disk-space bootstrap.

theorem NavierStokes.PositiveAxisExistence.solution_hasDerivAt {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 : VolterraRegularity.SmoothCoefficientData R U A₀ A₁ f) {r : ℝ} (hr : r ∈ VolterraRegularity.radialDomain R) {z : ℂ} (hz : z ∈ U) (i : Fin 6) : HasDerivAt (fun (s : ℝ) => W s z i) (NilpotentVolterra.equationRHS A₀ A₁ f W r z i - ↑(VolterraAnalyticBounds.exponent i) • NilpotentVolterra.weightedMean (VolterraAnalyticBounds.exponent i) (fun (s : ℝ) => NilpotentVolterra.equationRHS A₀ A₁ f W s z i) r) r

The actual symmetric solution has the regular, nonsingular derivative formula at every interior radius, including the axis.

theorem NavierStokes.PositiveAxisExistence.solution_differential_equation {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 : VolterraRegularity.SmoothCoefficientData R U A₀ A₁ f) {r : ℝ} (hr : r ∈ VolterraRegularity.radialDomain R) (hr0 : r ≠ 0) {z : ℂ} (hz : z ∈ U) (i : Fin 6) : deriv (fun (s : ℝ) => W s z i) r + (↑(VolterraAnalyticBounds.exponent i) / r) • W r z i = NilpotentVolterra.equationRHS A₀ A₁ f W r z i

The singular first-order equation holds with genuine derivatives at every nonzero interior radius.

noncomputable def NavierStokes.PositiveAxisExistence.matrixOperator : Matrix (Fin 6) (Fin 6) ℂ →L[ℂ] VolterraAnalyticBounds.Vec →L[ℂ] VolterraAnalyticBounds.Vec

The standard matrix representation, as an actual bounded operator on the six-component space.

Equations

• NavierStokes.PositiveAxisExistence.matrixOperator = ↑(Matrix.toLin'.trans LinearMap.toContinuousLinearMap).toContinuousLinearEquiv

@[simp]

theorem NavierStokes.PositiveAxisExistence.matrixOperator_apply (A : Matrix (Fin 6) (Fin 6) ℂ) (v : VolterraAnalyticBounds.Vec) : (matrixOperator A) v = A.mulVec v

@[simp]

theorem NavierStokes.PositiveAxisExistence.matrixOperator_toMatrix (A : Matrix (Fin 6) (Fin 6) ℂ) : LinearMap.toMatrix' ↑(matrixOperator A) = A

noncomputable def NavierStokes.PositiveAxisExistence.matrixPath (R : ℝ) (A : VolterraAnalyticBounds.Coeff) : ℂ → VolterraParity.SymmetricCoefficientPath R

Packaging the actual radial matrix coefficient in the compact path space.

Equations

• NavierStokes.PositiveAxisExistence.matrixPath R A = NavierStokes.CompactSmoothFamily.family (Set.Icc (-R) R) fun (p : ℂ × ℝ) => NavierStokes.PositiveAxisExistence.matrixOperator (A p.2 p.1)

noncomputable def NavierStokes.PositiveAxisExistence.forcingPath (R : ℝ) (f : VolterraAnalyticBounds.Field) : ℂ → VolterraParity.SymmetricPath R VolterraAnalyticBounds.Vec

Packaging the actual forcing in the compact path space.

Equations

• NavierStokes.PositiveAxisExistence.forcingPath R f = NavierStokes.CompactSmoothFamily.family (Set.Icc (-R) R) fun (p : ℂ × ℝ) => f p.2 p.1

theorem NavierStokes.PositiveAxisExistence.matrixPath_apply {R : ℝ} {A : VolterraAnalyticBounds.Coeff} {z : ℂ} (hA : Continuous fun (r : ↑(Set.Icc (-R) R)) => A (↑r) z) (r : ↑(Set.Icc (-R) R)) : (matrixPath R A z) r = matrixOperator (A (↑r) z)

theorem NavierStokes.PositiveAxisExistence.forcingPath_apply {R : ℝ} {f : VolterraAnalyticBounds.Field} {z : ℂ} (hf : Continuous fun (r : ↑(Set.Icc (-R) R)) => f (↑r) z) (r : ↑(Set.Icc (-R) R)) : (forcingPath R f z) r = f (↑r) z

theorem NavierStokes.PositiveAxisExistence.raw_matrixPath {R : ℝ} (hR : 0 ≤ R) {A : VolterraAnalyticBounds.Coeff} {z : ℂ} (hA : Continuous fun (r : ↑(Set.Icc (-R) R)) => A (↑r) z) {r : ℝ} (hr : r ∈ Set.Icc (-R) R) : VolterraParity.symmetricRawCoefficient hR (matrixPath R A) r z = A r z

theorem NavierStokes.PositiveAxisExistence.raw_forcingPath {R : ℝ} (hR : 0 ≤ R) {f : VolterraAnalyticBounds.Field} {z : ℂ} (hf : Continuous fun (r : ↑(Set.Icc (-R) R)) => f (↑r) z) {r : ℝ} (hr : r ∈ Set.Icc (-R) R) : VolterraParity.symmetricRawField hR (forcingPath R f) r z = f r z

theorem NavierStokes.PositiveAxisExistence.matrixPath_shape {R : ℝ} (hR : 0 ≤ R) {A : VolterraAnalyticBounds.Coeff} (hA : VolterraAnalyticBounds.DerivativeShape A) : VolterraAnalyticBounds.DerivativeShape (VolterraParity.symmetricRawCoefficient hR (matrixPath R A))

theorem NavierStokes.PositiveAxisExistence.scaled_mem_symmetricInterval {R r t : ℝ} (hr : r ∈ Set.Icc (-R) R) (ht : t ∈ Set.Icc 0 1) : t * r ∈ Set.Icc (-R) R

theorem NavierStokes.PositiveAxisExistence.solution_change_data {R : ℝ} {U : Set ℂ} {A₀ A₁ B₀ B₁ : VolterraAnalyticBounds.Coeff} {f g W : VolterraAnalyticBounds.Field} (h : VolterraParity.IsSymmetricIntegralSolution R U A₀ A₁ f W) (h₀ : ∀ r ∈ Set.Icc (-R) R, ∀ z ∈ U, A₀ r z = B₀ r z) (h₁ : ∀ r ∈ Set.Icc (-R) R, ∀ z ∈ U, A₁ r z = B₁ r z) (hf : ∀ r ∈ Set.Icc (-R) R, ∀ z ∈ U, f r z = g r z) : VolterraParity.IsSymmetricIntegralSolution R U B₀ B₁ g W

structure NavierStokes.PositiveAxisExistence.SmoothHolomorphicSystem (T : ℝ) (U : Set ℂ) (A₀ A₁ : VolterraAnalyticBounds.Coeff) (f : VolterraAnalyticBounds.Field) : Prop

Smoothness and parameter holomorphy of the given coefficients. These are hypotheses only on input functions.

• smooth : VolterraRegularity.SmoothCoefficientData T U A₀ A₁ f
• zeroth_holomorphic (r : ℝ) : r ∈ VolterraRegularity.radialDomain T → DifferentiableOn ℂ (A₀ r) U
• first_holomorphic (r : ℝ) : r ∈ VolterraRegularity.radialDomain T → DifferentiableOn ℂ (A₁ r) U
• forcing_holomorphic (r : ℝ) : r ∈ VolterraRegularity.radialDomain T → DifferentiableOn ℂ (f r) U

theorem NavierStokes.PositiveAxisExistence.symmetricInterval_subset_radialDomain {R T : ℝ} (hRT : R < T) : Set.Icc (-R) R ⊆ VolterraRegularity.radialDomain T

theorem NavierStokes.PositiveAxisExistence.radialDomain_mono {R T : ℝ} (hRT : R ≤ T) : VolterraRegularity.radialDomain R ⊆ VolterraRegularity.radialDomain T

theorem NavierStokes.PositiveAxisExistence.SmoothHolomorphicSystem.restrict {R T : ℝ} {U : Set ℂ} {A₀ A₁ : VolterraAnalyticBounds.Coeff} {f : VolterraAnalyticBounds.Field} (h : SmoothHolomorphicSystem T U A₀ A₁ f) (hRT : R ≤ T) : SmoothHolomorphicSystem R U A₀ A₁ f

theorem NavierStokes.PositiveAxisExistence.matrixPath_holomorphic {R T : ℝ} (hRT : R < T) {U : Set ℂ} (hU : IsOpen U) {A : VolterraAnalyticBounds.Coeff} (hA : ∀ (i j : Fin 6), ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => A p.1 p.2 i j) (VolterraRegularity.radialDomain T ×ˢ U)) (hhol : ∀ r ∈ VolterraRegularity.radialDomain T, DifferentiableOn ℂ (A r) U) : DifferentiableOn ℂ (matrixPath R A) U

theorem NavierStokes.PositiveAxisExistence.forcingPath_holomorphic {R T : ℝ} (hRT : R < T) {U : Set ℂ} (hU : IsOpen U) {f : VolterraAnalyticBounds.Field} (hf : ∀ (i : Fin 6), ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => f p.1 p.2 i) (VolterraRegularity.radialDomain T ×ˢ U)) (hhol : ∀ r ∈ VolterraRegularity.radialDomain T, DifferentiableOn ℂ (f r) U) : DifferentiableOn ℂ (forcingPath R f) U

theorem NavierStokes.PositiveAxisExistence.matrix_slice_continuous {R T : ℝ} (hRT : R < T) {U : Set ℂ} {A : VolterraAnalyticBounds.Coeff} (hA : ∀ (i j : Fin 6), ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => A p.1 p.2 i j) (VolterraRegularity.radialDomain T ×ˢ U)) {z : ℂ} (hz : z ∈ U) : Continuous fun (r : ↑(Set.Icc (-R) R)) => A (↑r) z

theorem NavierStokes.PositiveAxisExistence.forcing_slice_continuous {R T : ℝ} (hRT : R < T) {U : Set ℂ} {f : VolterraAnalyticBounds.Field} (hf : ∀ (i : Fin 6), ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => f p.1 p.2 i) (VolterraRegularity.radialDomain T ×ˢ U)) {z : ℂ} (hz : z ∈ U) : Continuous fun (r : ↑(Set.Icc (-R) R)) => f (↑r) z

noncomputable def NavierStokes.PositiveAxisExistence.assembledSolution {R : ℝ} (hR : 0 ≤ R) (A₀ A₁ : VolterraAnalyticBounds.Coeff) (f : VolterraAnalyticBounds.Field) : VolterraAnalyticBounds.Field

The actual canonical solution for raw matrix coefficients.

Equations

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

theorem NavierStokes.PositiveAxisExistence.assembledSolution_spec {R T : ℝ} (hR : 0 ≤ R) (hRT : R < T) {U : Set ℂ} (hU : IsOpen U) {A₀ A₁ : VolterraAnalyticBounds.Coeff} {f : VolterraAnalyticBounds.Field} (hdata : SmoothHolomorphicSystem T U A₀ A₁ f) (hshape : VolterraAnalyticBounds.DerivativeShape A₁) : VolterraParity.IsSymmetricIntegralSolution R U A₀ A₁ f (assembledSolution hR A₀ A₁ f)

theorem NavierStokes.PositiveAxisExistence.assembledSolution_parity {R T : ℝ} (hR : 0 ≤ R) (hRT : R < T) {U : Set ℂ} (hU : IsOpen U) {A₀ A₁ : VolterraAnalyticBounds.Coeff} {f : VolterraAnalyticBounds.Field} (hdata : SmoothHolomorphicSystem T U A₀ A₁ f) (hshape : VolterraAnalyticBounds.DerivativeShape A₁) (hp₀ : VolterraParity.CoefficientParity A₀) (hp₁ : VolterraParity.CoefficientParity A₁) (hpf : VolterraParity.ForcingParity f) {r : ℝ} (hr : r ∈ Set.Icc (-R) R) {z : ℂ} (hz : z ∈ U) : assembledSolution hR A₀ A₁ f (-r) z = VolterraParity.parityVec (assembledSolution hR A₀ A₁ f r z)

theorem NavierStokes.PositiveAxisExistence.solution_jointly_smooth {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 : VolterraRegularity.SmoothCoefficientData R U A₀ A₁ f) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => W p.1 p.2) (VolterraRegularity.radialDomain R ×ˢ U)

The disk-valued radial bootstrap and the Cauchy integral combine to give joint real smoothness, rather than merely separate smoothness.

structure NavierStokes.PositiveAxisExistence.LowerInputRegularity (T : ℝ) (U : Set ℂ) (h : ℂ) (F : PositiveAxisSystem.CoefficientData) : Prop

Transparent regularity assumptions on the eleven finite lower-order input functions. Smoothness is required of the signed square pullback, so there is no artificial requirement on a negative-X extension.

• radial_smooth (i : Fin 11) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => F i (p.1 ^ 2, p.2)) (VolterraRegularity.radialDomain T ×ˢ U)
• holomorphic (r : ℝ) : r ∈ VolterraRegularity.radialDomain T → ∀ (i : Fin 11), DifferentiableOn ℂ (fun (z : ℂ) => F i (r ^ 2, z)) U
• denominator (z : ℂ) : z ∈ U → PositiveAxisSystem.ell h z ≠ 0

theorem NavierStokes.PositiveAxisExistence.LowerInputRegularity.system {T : ℝ} {U : Set ℂ} (hU : IsOpen U) {h : ℂ} (lam C : ℂ) {F : PositiveAxisSystem.CoefficientData} (hF : LowerInputRegularity T U h F) : SmoothHolomorphicSystem T U (PositiveAxisSystem.coefficient0 h lam C F) (PositiveAxisSystem.coefficient1 h F) (PositiveAxisSystem.sourceField h C F)

noncomputable def NavierStokes.PositiveAxisExistence.positiveSolution {R : ℝ} (hR : 0 ≤ R) (h lam C : ℂ) (F : PositiveAxisSystem.CoefficientData) : VolterraAnalyticBounds.Field

The concrete series solution for the explicit positive-order matrices.

Equations

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

theorem NavierStokes.PositiveAxisExistence.positiveSolution_spec {R T : ℝ} (hR : 0 ≤ R) (hRT : R < T) {U : Set ℂ} (hU : IsOpen U) {h : ℂ} (lam C : ℂ) {F : PositiveAxisSystem.CoefficientData} (hF : LowerInputRegularity T U h F) : VolterraParity.IsSymmetricIntegralSolution R U (PositiveAxisSystem.coefficient0 h lam C F) (PositiveAxisSystem.coefficient1 h F) (PositiveAxisSystem.sourceField h C F) (positiveSolution hR h lam C F)

theorem NavierStokes.PositiveAxisExistence.positiveSolution_jointly_smooth {R T : ℝ} (hR : 0 ≤ R) (hRT : R < T) {U : Set ℂ} (hU : IsOpen U) {h : ℂ} (lam C : ℂ) {F : PositiveAxisSystem.CoefficientData} (hF : LowerInputRegularity T U h F) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => positiveSolution hR h lam C F p.1 p.2) (VolterraRegularity.radialDomain R ×ˢ U)

theorem NavierStokes.PositiveAxisExistence.positiveSolution_parity {R T : ℝ} (hR : 0 ≤ R) (hRT : R < T) {U : Set ℂ} (hU : IsOpen U) {h : ℂ} (lam C : ℂ) {F : PositiveAxisSystem.CoefficientData} (hF : LowerInputRegularity T U h F) {r : ℝ} (hr : r ∈ Set.Icc (-R) R) {z : ℂ} (hz : z ∈ U) : positiveSolution hR h lam C F (-r) z = VolterraParity.parityVec (positiveSolution hR h lam C F r z)

theorem NavierStokes.PositiveAxisExistence.positiveSolution_equation {R T : ℝ} (hR : 0 ≤ R) (hRT : R < T) {U : Set ℂ} (hU : IsOpen U) {h : ℂ} (lam C : ℂ) {F : PositiveAxisSystem.CoefficientData} (hF : LowerInputRegularity T U h F) {r : ℝ} (hr : r ∈ VolterraRegularity.radialDomain R) (hr0 : r ≠ 0) {z : ℂ} (hz : z ∈ U) (i : Fin 6) : deriv (fun (s : ℝ) => positiveSolution hR h lam C F s z i) r + (↑(VolterraAnalyticBounds.exponent i) / r) • positiveSolution hR h lam C F r z i = NilpotentVolterra.equationRHS (PositiveAxisSystem.coefficient0 h lam C F) (PositiveAxisSystem.coefficient1 h F) (PositiveAxisSystem.sourceField h C F) (positiveSolution hR h lam C F) r z i

noncomputable def NavierStokes.PositiveAxisExistence.realParameterDomain (U : Set ℂ) : Set ℝ

Real parameter domain, given by {eta | (eta : ℂ) ∈ U}.

Equations

• NavierStokes.PositiveAxisExistence.realParameterDomain U = {eta : ℝ | ↑eta ∈ U}

theorem NavierStokes.PositiveAxisExistence.realParameterDomain_isOpen {U : Set ℂ} (hU : IsOpen U) : IsOpen (realParameterDomain U)

noncomputable def NavierStokes.PositiveAxisExistence.realRadialComponent (W : VolterraAnalyticBounds.Field) (i : Fin 6) (p : ℝ × ℝ) : ℝ

Real radial component, given by (W p.2 (p.1 : ℂ) i).re.

Equations

• NavierStokes.PositiveAxisExistence.realRadialComponent W i p = (W p.2 (↑p.1) i).re

noncomputable def NavierStokes.PositiveAxisExistence.xProfile (W : VolterraAnalyticBounds.Field) (i : Fin 6) (p : ℝ × ℝ) : ℝ

Actual profiles, with the physical coordinate order (X,eta).

Equations

• NavierStokes.PositiveAxisExistence.xProfile W i p = NavierStokes.ParametricEvenDescent.descend (NavierStokes.PositiveAxisExistence.realRadialComponent W i) (p.2, p.1)

@[simp]

theorem NavierStokes.PositiveAxisExistence.xProfile_apply (W : VolterraAnalyticBounds.Field) (i : Fin 6) (X eta : ℝ) : xProfile W i (X, eta) = (W (√X) (↑eta) i).re

theorem NavierStokes.PositiveAxisExistence.realRadialComponent_smooth {R : ℝ} {U : Set ℂ} {W : VolterraAnalyticBounds.Field} (hW : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => W p.1 p.2) (VolterraRegularity.radialDomain R ×ˢ U)) (i : Fin 6) : ContDiffOn ℝ (↑⊤) (realRadialComponent W i) (realParameterDomain U ×ˢ Set.Ioo (-R) R)

theorem NavierStokes.PositiveAxisExistence.realRadialComponent_even {R : ℝ} {U : Set ℂ} {W : VolterraAnalyticBounds.Field} (hparity : ∀ r ∈ Set.Icc (-R) R, ∀ z ∈ U, W (-r) z = VolterraParity.parityVec (W r z)) (i : Fin 6) (hi : ↑i < 4) (eta : ℝ) : eta ∈ realParameterDomain U → ∀ r ∈ Set.Ioo (-R) R, realRadialComponent W i (eta, -r) = realRadialComponent W i (eta, r)

theorem NavierStokes.PositiveAxisExistence.xProfile_smooth {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) {W : VolterraAnalyticBounds.Field} (hW : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => W p.1 p.2) (VolterraRegularity.radialDomain R ×ˢ U)) (hparity : ∀ r ∈ Set.Icc (-R) R, ∀ z ∈ U, W (-r) z = VolterraParity.parityVec (W r z)) (i : Fin 6) (hi : ↑i < 4) : ContDiffOn ℝ (↑⊤) (xProfile W i) (Set.Ico 0 (R ^ 2) ×ˢ realParameterDomain U)

theorem NavierStokes.PositiveAxisExistence.xProfile_square {R : ℝ} {U : Set ℂ} {W : VolterraAnalyticBounds.Field} (hparity : ∀ r ∈ Set.Icc (-R) R, ∀ z ∈ U, W (-r) z = VolterraParity.parityVec (W r z)) (i : Fin 6) (hi : ↑i < 4) {eta r : ℝ} (heta : eta ∈ realParameterDomain U) (hr : r ∈ Set.Ioo (-R) R) : xProfile W i (r ^ 2, eta) = (W r (↑eta) i).re

theorem NavierStokes.PositiveAxisExistence.xProfile_axis_zero {U : Set ℂ} {W : VolterraAnalyticBounds.Field} (haxis : ∀ z ∈ U, W 0 z = 0) (i : Fin 6) {eta : ℝ} (heta : eta ∈ realParameterDomain U) : xProfile W i (0, eta) = 0

theorem NavierStokes.PositiveAxisExistence.xProfile_axis_jet {R : ℝ} (hR : 0 < R) {U : Set ℂ} {W : VolterraAnalyticBounds.Field} (hW : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => W p.1 p.2) (VolterraRegularity.radialDomain R ×ˢ U)) (hparity : ∀ r ∈ Set.Icc (-R) R, ∀ z ∈ U, W (-r) z = VolterraParity.parityVec (W r z)) (i : Fin 6) (hi : ↑i < 4) {eta : ℝ} (heta : eta ∈ realParameterDomain U) (n : ℕ) : iteratedDerivWithin n (fun (X : ℝ) => xProfile W i (X, eta)) (Set.Ici 0) 0 = (↑n.factorial / ↑(2 * n).factorial) • iteratedDeriv (2 * n) (fun (r : ℝ) => (W r (↑eta) i).re) 0

@[reducible, inline]

abbrev NavierStokes.PositiveAxisExistence.RealCoefficientData : Type

Real coefficient data: an abbreviation for Fin 11 → ℝ × ℝ → ℝ.

Equations

• NavierStokes.PositiveAxisExistence.RealCoefficientData = (Fin 11 → ℝ × ℝ → ℝ)

@[reducible, inline]

abbrev NavierStokes.PositiveAxisExistence.RealField : Type

Real field: an abbreviation for ℝ → ℝ → Fin 6 → ℝ.

Equations

• NavierStokes.PositiveAxisExistence.RealField = (ℝ → ℝ → Fin 6 → ℝ)

noncomputable def NavierStokes.PositiveAxisExistence.realBase (G : RealCoefficientData) (p : ℝ × ℝ) : PositiveAxisSystem.BaseJet ℝ

Real base, given by ⟨⟨G 0 p, G 1 p, 0, G 2 p⟩, ⟨G 3 p, G 4 p, 0, G 5 p⟩, G 6 p⟩.

Equations

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

noncomputable def NavierStokes.PositiveAxisExistence.realSource (G : RealCoefficientData) (p : ℝ × ℝ) : PositiveAxisSystem.SourceJet ℝ

Real source, given by ⟨G 7 p, G 8 p, G 9 p, G 10 p⟩.

Equations

• NavierStokes.PositiveAxisExistence.realSource G p = { angular := G 7 p, axial := G 8 p, pressureProduct := G 9 p, omegaQuotient := G 10 p }

def NavierStokes.PositiveAxisExistence.RealCompatible (R : ℝ) (U : Set ℂ) (F : PositiveAxisSystem.CoefficientData) (G : RealCoefficientData) : Prop

The complex inputs restrict to the given real finite input jets on the positive physical domain. Their smooth radial extension supplies the axis limits, without referring to ordinary derivatives of a negative-X continuation.

Equations

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

theorem NavierStokes.PositiveAxisExistence.RealCompatible.base {R : ℝ} {U : Set ℂ} {F : PositiveAxisSystem.CoefficientData} {G : RealCoefficientData} (h : RealCompatible R U F G) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) (heta : eta ∈ realParameterDomain U) : PositiveAxisSystem.coefficientBase F X ↑eta = PositiveAxisSystem.complexBase (realBase G (X, eta))

theorem NavierStokes.PositiveAxisExistence.RealCompatible.source {R : ℝ} {U : Set ℂ} {F : PositiveAxisSystem.CoefficientData} {G : RealCoefficientData} (h : RealCompatible R U F G) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) (heta : eta ∈ realParameterDomain U) : PositiveAxisSystem.coefficientSource F X ↑eta = PositiveAxisSystem.complexSource (realSource G (X, eta))

theorem NavierStokes.PositiveAxisExistence.square_mem_Ico {R r : ℝ} (hr : r ∈ Set.Ioo (-R) R) : r ^ 2 ∈ Set.Ico 0 (R ^ 2)

def NavierStokes.PositiveAxisExistence.RealSixSystem (R : ℝ) (J : Set ℝ) (h lam C : ℝ) (G : RealCoefficientData) (w : RealField) : Prop

The genuine real first-order system, with all six ordinary derivatives.

Equations

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

theorem NavierStokes.PositiveAxisExistence.positiveSolution_real_system {R T : ℝ} (hR : 0 < R) (hRT : R < T) {U : Set ℂ} (hU : IsOpen U) (h lam C : ℝ) {F : PositiveAxisSystem.CoefficientData} (hF : LowerInputRegularity T U (↑h) F) {G : RealCoefficientData} (hreal : RealCompatible R U F G) : RealSixSystem R (realParameterDomain U) h lam C G (PositiveAxisSystem.realTrace (positiveSolution ⋯ (↑h) (↑lam) (↑C) F))

theorem NavierStokes.PositiveAxisExistence.matrixRHS_first_rows {K : Type u_1} [Field K] (h lam C r eta : K) (b : PositiveAxisSystem.BaseJet K) (s : PositiveAxisSystem.SourceJet K) (w v : Fin 6 → K) : PositiveAxisSystem.matrixRHS h lam C r eta b s w v 0 = w 4 ∧ PositiveAxisSystem.matrixRHS h lam C r eta b s w v 1 = w 5

The first two rows recover the radial derivative coordinates without using the input jets.

theorem NavierStokes.PositiveAxisExistence.RealSixSystem.first_derivative {R : ℝ} {J : Set ℝ} {h lam C : ℝ} {G : RealCoefficientData} {w : RealField} (hw : RealSixSystem R J h lam C G w) {r eta : ℝ} (hr : r ∈ Set.Ioo (-R) R) (hr0 : r ≠ 0) (heta : eta ∈ J) : deriv (fun (s : ℝ) => w s eta 0) r = w r eta 4 ∧ deriv (fun (s : ℝ) => w s eta 1) r = w r eta 5

theorem NavierStokes.PositiveAxisExistence.xProfile_contDiffAt {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) {W : VolterraAnalyticBounds.Field} (hW : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => W p.1 p.2) (VolterraRegularity.radialDomain R ×ˢ U)) (hparity : ∀ r ∈ Set.Icc (-R) R, ∀ z ∈ U, W (-r) z = VolterraParity.parityVec (W r z)) (i : Fin 6) (hi : ↑i < 4) {r eta : ℝ} (hr : r ∈ Set.Ioo (-R) R) (hr0 : r ≠ 0) (heta : eta ∈ realParameterDomain U) : ContDiffAt ℝ (↑⊤) (xProfile W i) (r ^ 2, eta)

theorem NavierStokes.PositiveAxisExistence.xProfile_vector_eq {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) {W : VolterraAnalyticBounds.Field} (hW : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => W p.1 p.2) (VolterraRegularity.radialDomain R ×ˢ U)) (hparity : ∀ r ∈ Set.Icc (-R) R, ∀ z ∈ U, W (-r) z = VolterraParity.parityVec (W r z)) {h lam C : ℝ} {G : RealCoefficientData} (heq : RealSixSystem R (realParameterDomain U) h lam C G (PositiveAxisSystem.realTrace W)) {r eta : ℝ} (hr : r ∈ Set.Ioo (-R) R) (hr0 : r ≠ 0) (heta : eta ∈ realParameterDomain U) : PositiveAxisSystem.profileVector (xProfile W 0) (xProfile W 1) (xProfile W 2) (xProfile W 3) r eta = PositiveAxisSystem.realTrace W r eta

The last two Volterra components are the actual radial derivatives of the first two descended profiles; they are not independent jet variables.

theorem NavierStokes.PositiveAxisExistence.xProfiles_system {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) {W : VolterraAnalyticBounds.Field} (hW : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => W p.1 p.2) (VolterraRegularity.radialDomain R ×ˢ U)) (hparity : ∀ r ∈ Set.Icc (-R) R, ∀ z ∈ U, W (-r) z = VolterraParity.parityVec (W r z)) {h lam C : ℝ} {G : RealCoefficientData} (heq : RealSixSystem R (realParameterDomain U) h lam C G (PositiveAxisSystem.realTrace W)) {r eta : ℝ} (hr : r ∈ Set.Ioo (-R) R) (hr0 : r ≠ 0) (heta : eta ∈ realParameterDomain U) : PositiveAxisSystem.ProfileSystem h lam C r eta (realBase G (r ^ 2, eta)) (realSource G (r ^ 2, eta)) (xProfile W 0) (xProfile W 1) (xProfile W 2) (xProfile W 3)

The recovered profiles solve the true differentiated system.

theorem NavierStokes.PositiveAxisExistence.positiveSolution_profiles_system {R T : ℝ} (hR : 0 < R) (hRT : R < T) {U : Set ℂ} (hU : IsOpen U) (h lam C : ℝ) {F : PositiveAxisSystem.CoefficientData} (hF : LowerInputRegularity T U (↑h) F) {G : RealCoefficientData} (hreal : RealCompatible R U F G) {r eta : ℝ} (hr : r ∈ Set.Ioo (-R) R) (hr0 : r ≠ 0) (heta : eta ∈ realParameterDomain U) : have W := positiveSolution ⋯ (↑h) (↑lam) (↑C) F; PositiveAxisSystem.ProfileSystem h lam C r eta (realBase G (r ^ 2, eta)) (realSource G (r ^ 2, eta)) (xProfile W 0) (xProfile W 1) (xProfile W 2) (xProfile W 3)

noncomputable def NavierStokes.PositiveAxisExistence.lowerHistoryData (h : ℝ) (n : ℕ) (phi u beta : ℕ → SimilarityProfile.InnerProfile) (omegaQuotient : SimilarityProfile.InnerProfile) : RealCoefficientData

The eleven real inputs are computed from the given lower-order history. The unknown order is not used in the finite source, as proved separately by actualLowerSource_update.

Equations

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

noncomputable def NavierStokes.PositiveAxisExistence.newBeta (h : ℝ) (n : ℕ) (u k : SimilarityProfile.InnerProfile) : SimilarityProfile.InnerProfile

New beta, defined pointwise by betaValue h (slowPower h n) w.2 (actualJet u w) (actualJet k w).

Equations

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

def NavierStokes.PositiveAxisExistence.ExtendsPositiveOrder (h C : ℝ) (n : ℕ) (phi u beta : ℕ → SimilarityProfile.InnerProfile) (phiNew uNew k p omegaQuotient : SimilarityProfile.InnerProfile) (w : SimilarityProfile.InnerPoint) : Prop

The original positive-order convolution equations evaluated on the history after inserting the newly constructed profiles.

Equations

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

theorem NavierStokes.PositiveAxisExistence.profileSystem_lowerHistoryData (h lam C r eta : ℝ) (n : ℕ) (phi u beta : ℕ → SimilarityProfile.InnerProfile) (omegaQuotient phiNew uNew k p : SimilarityProfile.InnerProfile) : PositiveAxisSystem.ProfileSystem h lam C r eta (realBase (lowerHistoryData h n phi u beta omegaQuotient) (r ^ 2, eta)) (realSource (lowerHistoryData h n phi u beta omegaQuotient) (r ^ 2, eta)) phiNew uNew k p ↔ PositiveAxisSystem.ProfileSystem h lam C r eta (PositiveAxisSystem.baseAtOrderZero (fun (j : ℕ) => PositiveAxisSystem.actualJet (phi j) (r ^ 2, eta)) (fun (j : ℕ) => PositiveAxisSystem.actualJet (u j) (r ^ 2, eta)) fun (j : ℕ) => beta j (r ^ 2, eta)) (PositiveAxisSystem.actualLowerSource h n phi u beta omegaQuotient (r ^ 2, eta)) phiNew uNew k p

theorem NavierStokes.PositiveAxisExistence.positiveSolution_extends_order {R T : ℝ} (hR : 0 < R) (hRT : R < T) {U : Set ℂ} (hU : IsOpen U) (h C : ℝ) {n : ℕ} (hn : 0 < n) (phi u beta : ℕ → SimilarityProfile.InnerProfile) (omegaQuotient : SimilarityProfile.InnerProfile) {F : PositiveAxisSystem.CoefficientData} (hF : LowerInputRegularity T U (↑h) F) (hreal : RealCompatible R U F (lowerHistoryData h n phi u beta omegaQuotient)) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) (heta : eta ∈ realParameterDomain U) : have W := positiveSolution ⋯ (↑h) (↑(PositiveAxisSystem.slowPower h n)) (↑C) F; ExtendsPositiveOrder h C n phi u beta (xProfile W 0) (xProfile W 1) (xProfile W 2) (xProfile W 3) omegaQuotient (X, eta)

def NavierStokes.PositiveAxisExistence.SidePathSolution {R : ℝ} (hR : 0 ≤ R) (U : Set ℂ) (A₀ A₁ : VolterraAnalyticBounds.Coeff) (f : VolterraAnalyticBounds.Field) (V : Bool → ℂ → NilpotentVolterra.Path R) : Prop

A competing solution is given by actual holomorphic continuous paths on the positive and reflected negative radial intervals.

Equations

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

noncomputable def NavierStokes.PositiveAxisExistence.candidateLift {R : ℝ} (hR : 0 ≤ R) (A₀ A₁ : VolterraAnalyticBounds.Coeff) (f : VolterraAnalyticBounds.Field) (V : Bool → ℂ → NilpotentVolterra.Path R) : VolterraAnalyticBounds.Field

Candidate lift, constructed using glue.

Equations

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

theorem NavierStokes.PositiveAxisExistence.assembledSolution_unique {R T : ℝ} (hR : 0 ≤ R) (hRT : R < T) {U : Set ℂ} (hU : IsOpen U) {A₀ A₁ : VolterraAnalyticBounds.Coeff} {f : VolterraAnalyticBounds.Field} (hdata : SmoothHolomorphicSystem T U A₀ A₁ f) (hshape : VolterraAnalyticBounds.DerivativeShape A₁) {V : Bool → ℂ → NilpotentVolterra.Path R} (hV : SidePathSolution hR U A₀ A₁ f V) (r : ℝ) {z : ℂ} (hz : z ∈ U) : candidateLift hR A₀ A₁ f V r z = assembledSolution hR A₀ A₁ f r z

Actual uniqueness in the holomorphic continuous-path class. It is deduced from the decaying Volterra-word majorant, with no norm smallness.

structure NavierStokes.PositiveAxisExistence.IsPositiveOrderSolution (R : ℝ) (U : Set ℂ) (h C : ℝ) (n : ℕ) (phi u beta : ℕ → SimilarityProfile.InnerProfile) (omegaQuotient : SimilarityProfile.InnerProfile) (F : PositiveAxisSystem.CoefficientData) (W : VolterraAnalyticBounds.Field) : Prop

The actual positive-order output: a smooth symmetric six-component field, its physical squared-radius profiles, and their exact equations and axis jets. Uniqueness is stated separately below.

• integral : VolterraParity.IsSymmetricIntegralSolution R U (PositiveAxisSystem.coefficient0 (↑h) (↑(PositiveAxisSystem.slowPower h n)) (↑C) F) (PositiveAxisSystem.coefficient1 (↑h) F) (PositiveAxisSystem.sourceField (↑h) (↑C) F) W
• smooth : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => W p.1 p.2) (VolterraRegularity.radialDomain R ×ˢ U)
• parity (r : ℝ) : r ∈ Set.Icc (-R) R → ∀ z ∈ U, W (-r) z = VolterraParity.parityVec (W r z)
• equation (r : ℝ) : r ∈ VolterraRegularity.radialDomain R → r ≠ 0 → ∀ z ∈ U, ∀ (i : Fin 6), deriv (fun (s : ℝ) => W s z i) r + (↑(VolterraAnalyticBounds.exponent i) / r) • W r z i = NilpotentVolterra.equationRHS (PositiveAxisSystem.coefficient0 (↑h) (↑(PositiveAxisSystem.slowPower h n)) (↑C) F) (PositiveAxisSystem.coefficient1 (↑h) F) (PositiveAxisSystem.sourceField (↑h) (↑C) F) W r z i
• profiles_smooth (i : Fin 6) : ↑i < 4 → ContDiffOn ℝ (↑⊤) (xProfile W i) (Set.Ico 0 (R ^ 2) ×ˢ realParameterDomain U)
• profiles_zero (i : Fin 6) (eta : ℝ) : eta ∈ realParameterDomain U → xProfile W i (0, eta) = 0
• profiles_axis_jets (i : Fin 6) : ↑i < 4 → ∀ eta ∈ realParameterDomain U, ∀ (k : ℕ), iteratedDerivWithin k (fun (X : ℝ) => xProfile W i (X, eta)) (Set.Ici 0) 0 = (↑k.factorial / ↑(2 * k).factorial) • iteratedDeriv (2 * k) (fun (r : ℝ) => (W r (↑eta) i).re) 0
• positive_order (X : ℝ) : X ∈ Set.Ioo 0 (R ^ 2) → ∀ eta ∈ realParameterDomain U, ExtendsPositiveOrder h C n phi u beta (xProfile W 0) (xProfile W 1) (xProfile W 2) (xProfile W 3) omegaQuotient (X, eta)

theorem NavierStokes.PositiveAxisExistence.exists_positive_order_solution {R T : ℝ} (hR : 0 < R) (hRT : R < T) {U : Set ℂ} (hU : IsOpen U) (h C : ℝ) {n : ℕ} (hn : 0 < n) (phi u beta : ℕ → SimilarityProfile.InnerProfile) (omegaQuotient : SimilarityProfile.InnerProfile) {F : PositiveAxisSystem.CoefficientData} (hF : LowerInputRegularity T U (↑h) F) (hreal : RealCompatible R U F (lowerHistoryData h n phi u beta omegaQuotient)) : ∃ (W : VolterraAnalyticBounds.Field), IsPositiveOrderSolution R U h C n phi u beta omegaQuotient F W

Concrete positive-order existence from smooth radial, holomorphic parameter input jets of the lower history. No solution, convergence, positive-order equation, or output smoothness is an input assumption.

theorem NavierStokes.PositiveAxisExistence.positive_order_solution_unique {R T : ℝ} (hR : 0 ≤ R) (hRT : R < T) {U : Set ℂ} (hU : IsOpen U) (h C : ℝ) (n : ℕ) {F : PositiveAxisSystem.CoefficientData} (hF : LowerInputRegularity T U (↑h) F) {V : Bool → ℂ → NilpotentVolterra.Path R} (hV : SidePathSolution hR U (PositiveAxisSystem.coefficient0 (↑h) (↑(PositiveAxisSystem.slowPower h n)) (↑C) F) (PositiveAxisSystem.coefficient1 (↑h) F) (PositiveAxisSystem.sourceField (↑h) (↑C) F) V) (r : ℝ) {z : ℂ} (hz : z ∈ U) : candidateLift hR (PositiveAxisSystem.coefficient0 (↑h) (↑(PositiveAxisSystem.slowPower h n)) (↑C) F) (PositiveAxisSystem.coefficient1 (↑h) F) (PositiveAxisSystem.sourceField (↑h) (↑C) F) V r z = positiveSolution hR (↑h) (↑(PositiveAxisSystem.slowPower h n)) (↑C) F r z

Uniqueness for the same explicit lower-data problem, for any competing pair of actual holomorphic continuous-path integral solutions.

Radial divisibility and regular slow-order sources

This module removes the apparent 1/X singularities in the radial source of equation (22), using the actual differential operators from SimilarityProfile.

noncomputable def NavierStokes.AxisSourceRegularity.axisFactor (v : SimilarityProfile.InnerProfile) (w : SimilarityProfile.InnerPoint) : ℝ

Axis factor, given by w.1 * v w.

Equations

• NavierStokes.AxisSourceRegularity.axisFactor v w = w.1 * v w

theorem NavierStokes.AxisSourceRegularity.partialX_axisFactor {v : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hv : DifferentiableAt ℝ v w) : SimilarityProfile.partialX (axisFactor v) w = v w + w.1 * SimilarityProfile.partialX v w

theorem NavierStokes.AxisSourceRegularity.partialEta_axisFactor {v : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hv : DifferentiableAt ℝ v w) : SimilarityProfile.partialEta (axisFactor v) w = w.1 * SimilarityProfile.partialEta v w

theorem NavierStokes.AxisSourceRegularity.T_axisFactor (h b : ℝ) {v : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hv : DifferentiableAt ℝ v w) : SimilarityProfile.T h b (axisFactor v) w = w.1 * SimilarityProfile.T h (b - 1) v w

Factoring out X shifts the similarity exponent by one.

theorem NavierStokes.AxisSourceRegularity.Z_axisFactor (h b : ℝ) {v : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hv : DifferentiableAt ℝ v w) : SimilarityProfile.Z h b (axisFactor v) w = w.1 * SimilarityProfile.Z h (b - 1) v w

theorem NavierStokes.AxisSourceRegularity.Z_congr_germ (h b : ℝ) {f g : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hfg : f =ᶠ[nhds w] g) : SimilarityProfile.Z h b f w = SimilarityProfile.Z h b g w

theorem NavierStokes.AxisSourceRegularity.partialXX_axisFactor {v : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hv : ContDiffAt ℝ 2 v w) : SimilarityProfile.partialX (SimilarityProfile.partialX (axisFactor v)) w = 2 * SimilarityProfile.partialX v w + w.1 * SimilarityProfile.partialX (SimilarityProfile.partialX v) w

noncomputable def NavierStokes.AxisSourceRegularity.Z2 (h b : ℝ) (v : SimilarityProfile.InnerProfile) : SimilarityProfile.InnerProfile

Z2, given by Z h (b - D h) (Z h b v).

Equations

• NavierStokes.AxisSourceRegularity.Z2 h b v = NavierStokes.SimilarityProfile.Z h (b - NavierStokes.SimilarityProfile.D h) (NavierStokes.SimilarityProfile.Z h b v)

theorem NavierStokes.AxisSourceRegularity.Z2_axisFactor (h b : ℝ) {v : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hv : ContDiffAt ℝ 2 v w) (hL : SimilarityProfile.L h w.2 ≠ 0) : Z2 h b (axisFactor v) w = w.1 * Z2 h (b - 1) v w

theorem NavierStokes.AxisSourceRegularity.radial_advection_axisFactor {vi vj : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hvj : DifferentiableAt ℝ vj w) : axisFactor vi w * (SimilarityProfile.partialX (axisFactor vj) w - axisFactor vj w / (2 * w.1)) = w.1 * (vi w * (vj w / 2 + w.1 * SimilarityProfile.partialX vj w))

noncomputable def NavierStokes.AxisSourceRegularity.slowOrder (h : ℝ) (k : ℕ) : ℝ

Slow order, given by 2 * (k : ℝ) * h.

Equations

• NavierStokes.AxisSourceRegularity.slowOrder h k = 2 * ↑k * h

noncomputable def NavierStokes.AxisSourceRegularity.shiftedAxial (h : ℝ) (V : ℕ → SimilarityProfile.InnerProfile) : ℕ → SimilarityProfile.InnerProfile

Shifted axial as an element of ℕ → InnerProfile | 0 => fun _ => 0 | k + 1 => Z2 h (slowOrder h k) (V k).

Equations

• NavierStokes.AxisSourceRegularity.shiftedAxial h V 0 = fun (x : NavierStokes.SimilarityProfile.InnerPoint) => 0
• NavierStokes.AxisSourceRegularity.shiftedAxial h V k.succ = NavierStokes.AxisSourceRegularity.Z2 h (NavierStokes.AxisSourceRegularity.slowOrder h k) (V k)

noncomputable def NavierStokes.AxisSourceRegularity.shiftedAxialFactor (h : ℝ) (v : ℕ → SimilarityProfile.InnerProfile) : ℕ → SimilarityProfile.InnerProfile

Shifted axial factor as an element of ℕ → InnerProfile | 0 => fun _ => 0 | k + 1 => Z2 h (slowOrder h k - 1) (v k).

Equations

• NavierStokes.AxisSourceRegularity.shiftedAxialFactor h v 0 = fun (x : NavierStokes.SimilarityProfile.InnerPoint) => 0
• NavierStokes.AxisSourceRegularity.shiftedAxialFactor h v k.succ = NavierStokes.AxisSourceRegularity.Z2 h (NavierStokes.AxisSourceRegularity.slowOrder h k - 1) (v k)

noncomputable def NavierStokes.AxisSourceRegularity.omega (h : ℝ) (U V : ℕ → SimilarityProfile.InnerProfile) (k : ℕ) (w : SimilarityProfile.InnerPoint) : ℝ

The displayed Ω_k source before canceling its radial factor.

Equations

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

noncomputable def NavierStokes.AxisSourceRegularity.omegaDivX (h : ℝ) (U v : ℕ → SimilarityProfile.InnerProfile) (k : ℕ) (w : SimilarityProfile.InnerPoint) : ℝ

An explicit expression for Ω_k/X with no division by X.

Equations

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

theorem NavierStokes.AxisSourceRegularity.shiftedAxial_axisFactor (h : ℝ) (v : ℕ → SimilarityProfile.InnerProfile) (k : ℕ) (w : SimilarityProfile.InnerPoint) (hv : ∀ j ≤ k, ContDiffAt ℝ 2 (v j) w) (hL : SimilarityProfile.L h w.2 ≠ 0) : shiftedAxial h (fun (j : ℕ) => axisFactor (v j)) k w = w.1 * shiftedAxialFactor h v k w

theorem NavierStokes.AxisSourceRegularity.omega_axisFactor (h : ℝ) (U v : ℕ → SimilarityProfile.InnerProfile) (k : ℕ) (w : SimilarityProfile.InnerPoint) (hv : ∀ j ≤ k, ContDiffAt ℝ 2 (v j) w) (hL : SimilarityProfile.L h w.2 ≠ 0) : omega h U (fun (j : ℕ) => axisFactor (v j)) k w = w.1 * omegaDivX h U v k w

Every term in the actual finite Ω_k source has the factor X.

theorem NavierStokes.AxisSourceRegularity.omega_quotient_eq (h : ℝ) (U v : ℕ → SimilarityProfile.InnerProfile) (k : ℕ) (w : SimilarityProfile.InnerPoint) (hv : ∀ j ≤ k, ContDiffAt ℝ 2 (v j) w) (hL : SimilarityProfile.L h w.2 ≠ 0) (hX : w.1 ≠ 0) : omega h U (fun (j : ℕ) => axisFactor (v j)) k w / w.1 = omegaDivX h U v k w

theorem NavierStokes.AxisSourceRegularity.partialX_smooth {v : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hv : ContDiffAt ℝ (↑⊤) v w) : ContDiffAt ℝ (↑⊤) (SimilarityProfile.partialX v) w

theorem NavierStokes.AxisSourceRegularity.partialEta_smooth {v : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hv : ContDiffAt ℝ (↑⊤) v w) : ContDiffAt ℝ (↑⊤) (SimilarityProfile.partialEta v) w

theorem NavierStokes.AxisSourceRegularity.T_smooth (h b : ℝ) {v : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hv : ContDiffAt ℝ (↑⊤) v w) (hL : SimilarityProfile.L h w.2 ≠ 0) : ContDiffAt ℝ (↑⊤) (SimilarityProfile.T h b v) w

theorem NavierStokes.AxisSourceRegularity.Z_smooth (h b : ℝ) {v : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hv : ContDiffAt ℝ (↑⊤) v w) (hL : SimilarityProfile.L h w.2 ≠ 0) : ContDiffAt ℝ (↑⊤) (SimilarityProfile.Z h b v) w

theorem NavierStokes.AxisSourceRegularity.Z2_smooth (h b : ℝ) {v : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hv : ContDiffAt ℝ (↑⊤) v w) (hL : SimilarityProfile.L h w.2 ≠ 0) : ContDiffAt ℝ (↑⊤) (Z2 h b v) w

theorem NavierStokes.AxisSourceRegularity.antidiagonal_indices_le {i j k : ℕ} (hij : (i, j) ∈ Finset.antidiagonal k) : i ≤ k ∧ j ≤ k

theorem NavierStokes.AxisSourceRegularity.omegaDivX_smooth (h : ℝ) (U v : ℕ → SimilarityProfile.InnerProfile) (k : ℕ) (w : SimilarityProfile.InnerPoint) (hU : ∀ j ≤ k, ContDiffAt ℝ (↑⊤) (U j) w) (hv : ∀ j ≤ k, ContDiffAt ℝ (↑⊤) (v j) w) (hL : SimilarityProfile.L h w.2 ≠ 0) : ContDiffAt ℝ (↑⊤) (omegaDivX h U v k) w

The quotient formula is smooth at the axis, using only the finite input profiles occurring at this order. No division by the radial coordinate remains.

theorem NavierStokes.AxisSourceRegularity.omegaDivX_smooth_extension_at_axis (h : ℝ) (U v : ℕ → SimilarityProfile.InnerProfile) (k : ℕ) (η : ℝ) (hU : ∀ j ≤ k, ContDiffAt ℝ (↑⊤) (U j) (0, η)) (hv : ∀ j ≤ k, ContDiffAt ℝ (↑⊤) (v j) (0, η)) (hL : SimilarityProfile.L h η ≠ 0) : ContDiffAt ℝ (↑⊤) (omegaDivX h U v k) (0, η)

theorem NavierStokes.AxisSourceRegularity.partialX_analytic {v : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hv : AnalyticAt ℝ v w) : AnalyticAt ℝ (SimilarityProfile.partialX v) w

theorem NavierStokes.AxisSourceRegularity.partialEta_analytic {v : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hv : AnalyticAt ℝ v w) : AnalyticAt ℝ (SimilarityProfile.partialEta v) w

theorem NavierStokes.AxisSourceRegularity.T_analytic (h b : ℝ) {v : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hv : AnalyticAt ℝ v w) (hL : SimilarityProfile.L h w.2 ≠ 0) : AnalyticAt ℝ (SimilarityProfile.T h b v) w

theorem NavierStokes.AxisSourceRegularity.Z_analytic (h b : ℝ) {v : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hv : AnalyticAt ℝ v w) (hL : SimilarityProfile.L h w.2 ≠ 0) : AnalyticAt ℝ (SimilarityProfile.Z h b v) w

theorem NavierStokes.AxisSourceRegularity.Z2_analytic (h b : ℝ) {v : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hv : AnalyticAt ℝ v w) (hL : SimilarityProfile.L h w.2 ≠ 0) : AnalyticAt ℝ (Z2 h b v) w

theorem NavierStokes.AxisSourceRegularity.omegaDivX_analytic (h : ℝ) (U v : ℕ → SimilarityProfile.InnerProfile) (k : ℕ) (w : SimilarityProfile.InnerPoint) (hU : ∀ j ≤ k, AnalyticAt ℝ (U j) w) (hv : ∀ j ≤ k, AnalyticAt ℝ (v j) w) (hL : SimilarityProfile.L h w.2 ≠ 0) : AnalyticAt ℝ (omegaDivX h U v k) w

Joint analytic input germs give an analytic quotient germ, including at X=0.

Explicit finite jets and parameter-analytic source formulas

structure NavierStokes.AxisSourceRegularity.Jet2 (K : Type u_1) : Type u_1

Jet2 data, collecting value, dx, de, dxx, dxe, dex and their compatibility conditions.

• value : K

  Value of Jet2, of type K.

• dx : K

  Dx of Jet2, of type K.

• de : K

  De of Jet2, of type K.

• dxx : K

  Dxx of Jet2, of type K.

• dxe : K

  Dxe of Jet2, of type K.

• dex : K

  Dex of Jet2, of type K.

• dee : K

  Dee of Jet2, of type K.

noncomputable def NavierStokes.AxisSourceRegularity.profileJet (v : SimilarityProfile.InnerProfile) (w : SimilarityProfile.InnerPoint) : Jet2 ℝ

Profile jet, bundling value, dx, de, dxx and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.AxisSourceRegularity.jetL {K : Type u_1} [Field K] (h e : K) : K

Jet L, given by 1 - 2 * h * e ^ 2.

Equations

• NavierStokes.AxisSourceRegularity.jetL h e = 1 - 2 * h * e ^ 2

noncomputable def NavierStokes.AxisSourceRegularity.jetT {K : Type u_1} [Field K] (h b X e : K) (j : Jet2 K) : K

Jet T, given by (-b * j.value + (1 / 2 - h) * e * j.de + X * j.dx) / jetL h e.

Equations

• NavierStokes.AxisSourceRegularity.jetT h b X e j = (-b * j.value + (1 / 2 - h) * e * j.de + X * j.dx) / NavierStokes.AxisSourceRegularity.jetL h e

noncomputable def NavierStokes.AxisSourceRegularity.jetZNumerator {K : Type u_1} [Field K] (b X e : K) (j : Jet2 K) : K

Jet Z numerator, given by 2 * e * b * j.value + (1 - e ^ 2) * j.de - 2 * e * X * j.dx.

Equations

• NavierStokes.AxisSourceRegularity.jetZNumerator b X e j = 2 * e * b * j.value + (1 - e ^ 2) * j.de - 2 * e * X * j.dx

noncomputable def NavierStokes.AxisSourceRegularity.jetZNumeratorX {K : Type u_1} [Field K] (b X e : K) (j : Jet2 K) : K

Jet Z numerator X, given by 2 * e * b * j.dx + (1 - e ^ 2) * j.dex - 2 * e * (j.dx + X * j.dxx).

Equations

• NavierStokes.AxisSourceRegularity.jetZNumeratorX b X e j = 2 * e * b * j.dx + (1 - e ^ 2) * j.dex - 2 * e * (j.dx + X * j.dxx)

noncomputable def NavierStokes.AxisSourceRegularity.jetZNumeratorE {K : Type u_1} [Field K] (b X e : K) (j : Jet2 K) : K

Jet Z numerator E, given by `2 * b * j.value + 2 * e * b * j.de - 2 * e * j.de + (1 - e ^ 2)

• j.dee - 2 * X * j.dx - 2 * e * X * j.dxe`.

Equations

• NavierStokes.AxisSourceRegularity.jetZNumeratorE b X e j = 2 * b * j.value + 2 * e * b * j.de - 2 * e * j.de + (1 - e ^ 2) * j.dee - 2 * X * j.dx - 2 * e * X * j.dxe

noncomputable def NavierStokes.AxisSourceRegularity.jetZ {K : Type u_1} [Field K] (h b X e : K) (j : Jet2 K) : K

Jet Z, given by jetZNumerator b X e j / jetL h e.

Equations

• NavierStokes.AxisSourceRegularity.jetZ h b X e j = NavierStokes.AxisSourceRegularity.jetZNumerator b X e j / NavierStokes.AxisSourceRegularity.jetL h e

noncomputable def NavierStokes.AxisSourceRegularity.jetZX {K : Type u_1} [Field K] (h b X e : K) (j : Jet2 K) : K

Jet ZX, given by jetZNumeratorX b X e j / jetL h e.

Equations

• NavierStokes.AxisSourceRegularity.jetZX h b X e j = NavierStokes.AxisSourceRegularity.jetZNumeratorX b X e j / NavierStokes.AxisSourceRegularity.jetL h e

noncomputable def NavierStokes.AxisSourceRegularity.jetZE {K : Type u_1} [Field K] (h b X e : K) (j : Jet2 K) : K

Jet ZE, given by (jetZNumeratorE b X e j * jetL h e + 4 * h * e * jetZNumerator b X e j) / jetL h e ^ 2.

Equations

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

noncomputable def NavierStokes.AxisSourceRegularity.jetZ2 {K : Type u_1} [Field K] (h b X e : K) (j : Jet2 K) : K

Jet Z2, given by (2 * e * (b - (1 / 2 - h)) * jetZ h b X e j + (1 - e ^ 2) * jetZE h b X e j - 2 * e * X * jetZX h b X e j) / jetL h e.

Equations

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

theorem NavierStokes.AxisSourceRegularity.T_eq_jet (h b : ℝ) (v : SimilarityProfile.InnerProfile) (w : SimilarityProfile.InnerPoint) : SimilarityProfile.T h b v w = jetT h b w.1 w.2 (profileJet v w)

theorem NavierStokes.AxisSourceRegularity.Z_eq_jet (h b : ℝ) (v : SimilarityProfile.InnerProfile) (w : SimilarityProfile.InnerPoint) : SimilarityProfile.Z h b v w = jetZ h b w.1 w.2 (profileJet v w)

theorem NavierStokes.AxisSourceRegularity.Z_partials_eq_jet (h b : ℝ) {v : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hv : ContDiffAt ℝ 2 v w) (hL : SimilarityProfile.L h w.2 ≠ 0) : SimilarityProfile.partialX (SimilarityProfile.Z h b v) w = jetZX h b w.1 w.2 (profileJet v w) ∧ SimilarityProfile.partialEta (SimilarityProfile.Z h b v) w = jetZE h b w.1 w.2 (profileJet v w)

theorem NavierStokes.AxisSourceRegularity.Z2_eq_jet (h b : ℝ) {v : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hv : ContDiffAt ℝ 2 v w) (hL : SimilarityProfile.L h w.2 ≠ 0) : Z2 h b v w = jetZ2 h b w.1 w.2 (profileJet v w)

noncomputable def NavierStokes.AxisSourceRegularity.jetShifted {K : Type u_1} [Field K] (h X e : K) (v : ℕ → Jet2 K) : ℕ → K

Jet shifted as an element of ℕ → K | 0 => 0 | k + 1 => jetZ2 h (2 * (k : K) * h - 1) X e (v k).

Equations

• NavierStokes.AxisSourceRegularity.jetShifted h X e v 0 = 0
• NavierStokes.AxisSourceRegularity.jetShifted h X e v k.succ = NavierStokes.AxisSourceRegularity.jetZ2 h (2 * ↑k * h - 1) X e (v k)

noncomputable def NavierStokes.AxisSourceRegularity.jetOmegaDivX {K : Type u_1} [Field K] (h X e : K) (U : ℕ → K) (v : ℕ → Jet2 K) (k : ℕ) : K

The same regular source formula over any field, so complex parameter extensions use precisely the algebra verified for the real profile derivatives.

Equations

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

theorem NavierStokes.AxisSourceRegularity.omegaDivX_eq_jet (h : ℝ) (U v : ℕ → SimilarityProfile.InnerProfile) (k : ℕ) (w : SimilarityProfile.InnerPoint) (hv : ∀ j ≤ k, ContDiffAt ℝ 2 (v j) w) (hL : SimilarityProfile.L h w.2 ≠ 0) : omegaDivX h U v k w = jetOmegaDivX h w.1 w.2 (fun (j : ℕ) => U j w) (fun (j : ℕ) => profileJet (v j) w) k

structure NavierStokes.AxisSourceRegularity.AnalyticJetAt (J : ℂ → Jet2 ℂ) (e : ℂ) : Prop

Holomorphic extensions of the seven actual input jets. This is stronger than separate analyticity of v alone and is the precise parameter hypothesis used.

• value : AnalyticAt ℂ (fun (z : ℂ) => (J z).value) e
• dx : AnalyticAt ℂ (fun (z : ℂ) => (J z).dx) e
• de : AnalyticAt ℂ (fun (z : ℂ) => (J z).de) e
• dxx : AnalyticAt ℂ (fun (z : ℂ) => (J z).dxx) e
• dxe : AnalyticAt ℂ (fun (z : ℂ) => (J z).dxe) e
• dex : AnalyticAt ℂ (fun (z : ℂ) => (J z).dex) e
• dee : AnalyticAt ℂ (fun (z : ℂ) => (J z).dee) e

theorem NavierStokes.AxisSourceRegularity.jetL_analytic (h e : ℂ) : AnalyticAt ℂ (jetL h) e

theorem NavierStokes.AxisSourceRegularity.jetT_analytic (h b X : ℂ) {J : ℂ → Jet2 ℂ} {e : ℂ} (hJ : AnalyticJetAt J e) (hL : jetL h e ≠ 0) : AnalyticAt ℂ (fun (z : ℂ) => jetT h b X z (J z)) e

theorem NavierStokes.AxisSourceRegularity.jetZNumerator_analytic (b X : ℂ) {J : ℂ → Jet2 ℂ} {e : ℂ} (hJ : AnalyticJetAt J e) : AnalyticAt ℂ (fun (z : ℂ) => jetZNumerator b X z (J z)) e

theorem NavierStokes.AxisSourceRegularity.jetZNumeratorX_analytic (b X : ℂ) {J : ℂ → Jet2 ℂ} {e : ℂ} (hJ : AnalyticJetAt J e) : AnalyticAt ℂ (fun (z : ℂ) => jetZNumeratorX b X z (J z)) e

theorem NavierStokes.AxisSourceRegularity.jetZNumeratorE_analytic (b X : ℂ) {J : ℂ → Jet2 ℂ} {e : ℂ} (hJ : AnalyticJetAt J e) : AnalyticAt ℂ (fun (z : ℂ) => jetZNumeratorE b X z (J z)) e

theorem NavierStokes.AxisSourceRegularity.jetZ_analytic (h b X : ℂ) {J : ℂ → Jet2 ℂ} {e : ℂ} (hJ : AnalyticJetAt J e) (hL : jetL h e ≠ 0) : AnalyticAt ℂ (fun (z : ℂ) => jetZ h b X z (J z)) e

theorem NavierStokes.AxisSourceRegularity.jetZX_analytic (h b X : ℂ) {J : ℂ → Jet2 ℂ} {e : ℂ} (hJ : AnalyticJetAt J e) (hL : jetL h e ≠ 0) : AnalyticAt ℂ (fun (z : ℂ) => jetZX h b X z (J z)) e

theorem NavierStokes.AxisSourceRegularity.jetZE_analytic (h b X : ℂ) {J : ℂ → Jet2 ℂ} {e : ℂ} (hJ : AnalyticJetAt J e) (hL : jetL h e ≠ 0) : AnalyticAt ℂ (fun (z : ℂ) => jetZE h b X z (J z)) e

theorem NavierStokes.AxisSourceRegularity.jetZ2_analytic (h b X : ℂ) {J : ℂ → Jet2 ℂ} {e : ℂ} (hJ : AnalyticJetAt J e) (hL : jetL h e ≠ 0) : AnalyticAt ℂ (fun (z : ℂ) => jetZ2 h b X z (J z)) e

theorem NavierStokes.AxisSourceRegularity.jetOmegaDivX_analytic (h X : ℂ) (U : ℕ → ℂ → ℂ) (v : ℕ → ℂ → Jet2 ℂ) (k : ℕ) (e : ℂ) (hU : ∀ j ≤ k, AnalyticAt ℂ (U j) e) (hv : ∀ j ≤ k, AnalyticJetAt (v j) e) (hL : jetL h e ≠ 0) : AnalyticAt ℂ (fun (z : ℂ) => jetOmegaDivX h X z (fun (j : ℕ) => U j z) (fun (j : ℕ) => v j z) k) e

The finite quotient source is holomorphic in the parameter whenever the finite input jets have holomorphic extensions and the sole denominator is nonzero.

noncomputable def NavierStokes.AxisSourceRegularity.complexifyJet (j : Jet2 ℝ) : Jet2 ℂ

Complexify jet, bundling value, dx, de, dxx and the required compatibility proofs.

Equations

• NavierStokes.AxisSourceRegularity.complexifyJet j = { value := ↑j.value, dx := ↑j.dx, de := ↑j.de, dxx := ↑j.dxx, dxe := ↑j.dxe, dex := ↑j.dex, dee := ↑j.dee }

theorem NavierStokes.AxisSourceRegularity.jetT_ofReal (h b X e : ℝ) (j : Jet2 ℝ) : ↑(jetT h b X e j) = jetT (↑h) (↑b) (↑X) (↑e) (complexifyJet j)

The first-order jet time formula commutes with the real inclusion.

theorem NavierStokes.AxisSourceRegularity.jetZ_ofReal (h b X e : ℝ) (j : Jet2 ℝ) : ↑(jetZ h b X e j) = jetZ (↑h) (↑b) (↑X) (↑e) (complexifyJet j)

The first-order jet axial formula commutes with the real inclusion.

theorem NavierStokes.AxisSourceRegularity.jetZ2_ofReal (h b X e : ℝ) (j : Jet2 ℝ) : ↑(jetZ2 h b X e j) = jetZ2 (↑h) (↑b) (↑X) (↑e) (complexifyJet j)

The second-order jet axial formula commutes with the real inclusion.

theorem NavierStokes.AxisSourceRegularity.jetOmegaDivX_ofReal (h X e : ℝ) (U : ℕ → ℝ) (v : ℕ → Jet2 ℝ) (k : ℕ) : ↑(jetOmegaDivX h X e U v k) = jetOmegaDivX (↑h) (↑X) (↑e) (fun (j : ℕ) => ↑(U j)) (fun (j : ℕ) => complexifyJet (v j)) k

The holomorphic algebra uses the exact real source formula on real inputs.

theorem NavierStokes.AxisSourceRegularity.omegaDivX_complex_formula (h : ℝ) (U v : ℕ → SimilarityProfile.InnerProfile) (k : ℕ) (w : SimilarityProfile.InnerPoint) (hv : ∀ j ≤ k, ContDiffAt ℝ 2 (v j) w) (hL : SimilarityProfile.L h w.2 ≠ 0) : ↑(omegaDivX h U v k w) = jetOmegaDivX (↑h) (↑w.1) (↑w.2) (fun (j : ℕ) => ↑(U j w)) (fun (j : ℕ) => complexifyJet (profileJet (v j) w)) k

noncomputable def NavierStokes.AxisSourceRegularity.lowerPairs (n : ℕ) : Finset (ℕ × ℕ)

Lower pairs, given by (Finset.antidiagonal n).filter (fun ij => 0 < ij.1 ∧ 0 < ij.2).

Equations

• NavierStokes.AxisSourceRegularity.lowerPairs n = {ij ∈ Finset.antidiagonal n | 0 < ij.1 ∧ 0 < ij.2}

theorem NavierStokes.AxisSourceRegularity.lowerPairs_lt {n i j : ℕ} (hij : (i, j) ∈ lowerPairs n) : i < n ∧ j < n

noncomputable def NavierStokes.AxisSourceRegularity.lowerConvolution (a b : ℕ → SimilarityProfile.InnerProfile) (n : ℕ) (w : SimilarityProfile.InnerPoint) : ℝ

Lower convolution, given by ∑ ij ∈ lowerPairs n, a ij.1 w * b ij.2 w.

Equations

• NavierStokes.AxisSourceRegularity.lowerConvolution a b n w = ∑ ij ∈ NavierStokes.AxisSourceRegularity.lowerPairs n, a ij.1 w * b ij.2 w

noncomputable def NavierStokes.AxisSourceRegularity.previousOmegaDivX (h : ℝ) (U v : ℕ → SimilarityProfile.InnerProfile) : ℕ → SimilarityProfile.InnerProfile

Previous omega div X as an element of ℕ → InnerProfile | 0 => fun _ => 0 | k + 1 => omegaDivX h U v k.

Equations

• NavierStokes.AxisSourceRegularity.previousOmegaDivX h U v 0 = fun (x : NavierStokes.SimilarityProfile.InnerPoint) => 0
• NavierStokes.AxisSourceRegularity.previousOmegaDivX h U v k.succ = NavierStokes.AxisSourceRegularity.omegaDivX h U v k

noncomputable def NavierStokes.AxisSourceRegularity.lowerPressureSource (h C : ℝ) (φ U v : ℕ → SimilarityProfile.InnerProfile) (n : ℕ) (w : SimilarityProfile.InnerPoint) : ℝ

The known lower-order pressure source after its radial cancellation.

Equations

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

theorem NavierStokes.AxisSourceRegularity.lowerConvolution_smooth (a b : ℕ → SimilarityProfile.InnerProfile) (n : ℕ) (w : SimilarityProfile.InnerPoint) (ha : ∀ j < n, ContDiffAt ℝ (↑⊤) (a j) w) (hb : ∀ j < n, ContDiffAt ℝ (↑⊤) (b j) w) : ContDiffAt ℝ (↑⊤) (lowerConvolution a b n) w

theorem NavierStokes.AxisSourceRegularity.lowerPressureSource_smooth (h C : ℝ) (φ U v : ℕ → SimilarityProfile.InnerProfile) (n : ℕ) (w : SimilarityProfile.InnerPoint) (hφ : ∀ j < n, ContDiffAt ℝ (↑⊤) (φ j) w) (hU : ∀ j < n, ContDiffAt ℝ (↑⊤) (U j) w) (hv : ∀ j < n, ContDiffAt ℝ (↑⊤) (v j) w) (hL : SimilarityProfile.L h w.2 ≠ 0) : ContDiffAt ℝ (↑⊤) (lowerPressureSource h C φ U v n) w

theorem NavierStokes.AxisSourceRegularity.lowerConvolution_analytic (a b : ℕ → SimilarityProfile.InnerProfile) (n : ℕ) (w : SimilarityProfile.InnerPoint) (ha : ∀ j < n, AnalyticAt ℝ (a j) w) (hb : ∀ j < n, AnalyticAt ℝ (b j) w) : AnalyticAt ℝ (lowerConvolution a b n) w

theorem NavierStokes.AxisSourceRegularity.lowerPressureSource_analytic (h C : ℝ) (φ U v : ℕ → SimilarityProfile.InnerProfile) (n : ℕ) (w : SimilarityProfile.InnerPoint) (hφ : ∀ j < n, AnalyticAt ℝ (φ j) w) (hU : ∀ j < n, AnalyticAt ℝ (U j) w) (hv : ∀ j < n, AnalyticAt ℝ (v j) w) (hL : SimilarityProfile.L h w.2 ≠ 0) : AnalyticAt ℝ (lowerPressureSource h C φ U v n) w

theorem NavierStokes.AxisSourceRegularity.lowerPressureSource_eq_quotient (h C : ℝ) (φ U v : ℕ → SimilarityProfile.InnerProfile) (k : ℕ) (w : SimilarityProfile.InnerPoint) (hv : ∀ j ≤ k, ContDiffAt ℝ 2 (v j) w) (hL : SimilarityProfile.L h w.2 ≠ 0) (hX : w.1 ≠ 0) : lowerPressureSource h C φ U v (k + 1) w = C⁻¹ ^ 2 * lowerConvolution φ φ (k + 1) w - omega h U (fun (j : ℕ) => axisFactor (v j)) k w / w.1 / 2

The regular lower-order source agrees with the displayed pressure source away from the axis.

noncomputable def NavierStokes.AxisSourceRegularity.jetPreviousOmega {K : Type u_1} [Field K] (h X e : K) (U : ℕ → K) (v : ℕ → Jet2 K) : ℕ → K

Jet previous omega as an element of ℕ → K | 0 => 0 | k + 1 => jetOmegaDivX h X e U v k.

Equations

• NavierStokes.AxisSourceRegularity.jetPreviousOmega h X e U v 0 = 0
• NavierStokes.AxisSourceRegularity.jetPreviousOmega h X e U v k.succ = NavierStokes.AxisSourceRegularity.jetOmegaDivX h X e U v k

noncomputable def NavierStokes.AxisSourceRegularity.jetLowerPressureSource {K : Type u_1} [Field K] (h C X e : K) (φ U : ℕ → K) (v : ℕ → Jet2 K) (n : ℕ) : K

Parameter-analytic algebra for the same finite lower pressure source.

Equations

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

theorem NavierStokes.AxisSourceRegularity.lowerPressureSource_eq_jet (h C : ℝ) (φ U v : ℕ → SimilarityProfile.InnerProfile) (n : ℕ) (w : SimilarityProfile.InnerPoint) (hv : ∀ j < n, ContDiffAt ℝ 2 (v j) w) (hL : SimilarityProfile.L h w.2 ≠ 0) : lowerPressureSource h C φ U v n w = jetLowerPressureSource h C w.1 w.2 (fun (j : ℕ) => φ j w) (fun (j : ℕ) => U j w) (fun (j : ℕ) => profileJet (v j) w) n

theorem NavierStokes.AxisSourceRegularity.jetLowerPressureSource_ofReal (h C X e : ℝ) (φ U : ℕ → ℝ) (v : ℕ → Jet2 ℝ) (n : ℕ) : ↑(jetLowerPressureSource h C X e φ U v n) = jetLowerPressureSource (↑h) (↑C) (↑X) (↑e) (fun (j : ℕ) => ↑(φ j)) (fun (j : ℕ) => ↑(U j)) (fun (j : ℕ) => complexifyJet (v j)) n

theorem NavierStokes.AxisSourceRegularity.lowerPressureSource_complex_formula (h C : ℝ) (φ U v : ℕ → SimilarityProfile.InnerProfile) (n : ℕ) (w : SimilarityProfile.InnerPoint) (hv : ∀ j < n, ContDiffAt ℝ 2 (v j) w) (hL : SimilarityProfile.L h w.2 ≠ 0) : ↑(lowerPressureSource h C φ U v n w) = jetLowerPressureSource (↑h) (↑C) (↑w.1) (↑w.2) (fun (j : ℕ) => ↑(φ j w)) (fun (j : ℕ) => ↑(U j w)) (fun (j : ℕ) => complexifyJet (profileJet (v j) w)) n

theorem NavierStokes.AxisSourceRegularity.jetLowerPressureSource_analytic (h C X : ℂ) (φ U : ℕ → ℂ → ℂ) (v : ℕ → ℂ → Jet2 ℂ) (n : ℕ) (e : ℂ) (hφ : ∀ j < n, AnalyticAt ℂ (φ j) e) (hU : ∀ j < n, AnalyticAt ℂ (U j) e) (hv : ∀ j < n, AnalyticJetAt (v j) e) (hL : jetL h e ≠ 0) : AnalyticAt ℂ (fun (z : ℂ) => jetLowerPressureSource h C X z (fun (j : ℕ) => φ j z) (fun (j : ℕ) => U j z) (fun (j : ℕ) => v j z) n) e

Only previously constructed profiles, indexed strictly below n, are needed for holomorphy of the known source at order n.

The other finite lower-order transport sources

theorem NavierStokes.AxisSourceRegularity.transport_axisFactor (σ : ℝ) (v f : SimilarityProfile.InnerProfile) (w : SimilarityProfile.InnerPoint) (hX : w.1 ≠ 0) : axisFactor v w * (SimilarityProfile.partialX f w + σ * f w / w.1) = v w * (w.1 * SimilarityProfile.partialX f w + σ * f w)

noncomputable def NavierStokes.AxisSourceRegularity.shiftedProfileAxial (h b : ℝ) (f : ℕ → SimilarityProfile.InnerProfile) : ℕ → SimilarityProfile.InnerProfile

Shifted profile axial as an element of ℕ → InnerProfile | 0 => fun _ => 0 | k + 1 => Z2 h (b + slowOrder h k) (f k).

Equations

• NavierStokes.AxisSourceRegularity.shiftedProfileAxial h b f 0 = fun (x : NavierStokes.SimilarityProfile.InnerPoint) => 0
• NavierStokes.AxisSourceRegularity.shiftedProfileAxial h b f k.succ = NavierStokes.AxisSourceRegularity.Z2 h (b + NavierStokes.AxisSourceRegularity.slowOrder h k) (f k)

noncomputable def NavierStokes.AxisSourceRegularity.lowerTransportSource (h b σ : ℝ) (v U f : ℕ → SimilarityProfile.InnerProfile) (n : ℕ) (w : SimilarityProfile.InnerPoint) : ℝ

The finite known transport part of the angular row has σ=1, and that of the axial row has σ=0. The base exponents b are supplied separately.

Equations

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

theorem NavierStokes.AxisSourceRegularity.lowerTransportSource_eq_quotient (h b σ : ℝ) (v U f : ℕ → SimilarityProfile.InnerProfile) (n : ℕ) (w : SimilarityProfile.InnerPoint) (hX : w.1 ≠ 0) : lowerTransportSource h b σ v U f n w = ∑ ij ∈ lowerPairs n, (axisFactor (v ij.1) w * (SimilarityProfile.partialX (f ij.2) w + σ * f ij.2 w / w.1) + U ij.1 w * SimilarityProfile.Z h (b + slowOrder h ij.2) (f ij.2) w) - shiftedProfileAxial h b f n w

theorem NavierStokes.AxisSourceRegularity.lowerTransportSource_smooth (h b σ : ℝ) (v U f : ℕ → SimilarityProfile.InnerProfile) (n : ℕ) (w : SimilarityProfile.InnerPoint) (hv : ∀ j < n, ContDiffAt ℝ (↑⊤) (v j) w) (hU : ∀ j < n, ContDiffAt ℝ (↑⊤) (U j) w) (hf : ∀ j < n, ContDiffAt ℝ (↑⊤) (f j) w) (hL : SimilarityProfile.L h w.2 ≠ 0) : ContDiffAt ℝ (↑⊤) (lowerTransportSource h b σ v U f n) w

theorem NavierStokes.AxisSourceRegularity.lowerTransportSource_analytic (h b σ : ℝ) (v U f : ℕ → SimilarityProfile.InnerProfile) (n : ℕ) (w : SimilarityProfile.InnerPoint) (hv : ∀ j < n, AnalyticAt ℝ (v j) w) (hU : ∀ j < n, AnalyticAt ℝ (U j) w) (hf : ∀ j < n, AnalyticAt ℝ (f j) w) (hL : SimilarityProfile.L h w.2 ≠ 0) : AnalyticAt ℝ (lowerTransportSource h b σ v U f n) w

noncomputable def NavierStokes.AxisSourceRegularity.jetShiftedProfileAxial {K : Type u_1} [Field K] (h b X e : K) (f : ℕ → Jet2 K) : ℕ → K

Jet shifted profile axial as an element of ℕ → K | 0 => 0 | k + 1 => jetZ2 h (b + 2 * (k : K) * h) X e (f k).

Equations

• NavierStokes.AxisSourceRegularity.jetShiftedProfileAxial h b X e f 0 = 0
• NavierStokes.AxisSourceRegularity.jetShiftedProfileAxial h b X e f k.succ = NavierStokes.AxisSourceRegularity.jetZ2 h (b + 2 * ↑k * h) X e (f k)

noncomputable def NavierStokes.AxisSourceRegularity.jetLowerTransportSource {K : Type u_1} [Field K] (h b σ X e : K) (v U : ℕ → K) (f : ℕ → Jet2 K) (n : ℕ) : K

Jet lower transport source as an element of K.

Equations

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

theorem NavierStokes.AxisSourceRegularity.lowerTransportSource_eq_jet (h b σ : ℝ) (v U f : ℕ → SimilarityProfile.InnerProfile) (n : ℕ) (w : SimilarityProfile.InnerPoint) (hf : ∀ j < n, ContDiffAt ℝ 2 (f j) w) (hL : SimilarityProfile.L h w.2 ≠ 0) : lowerTransportSource h b σ v U f n w = jetLowerTransportSource h b σ w.1 w.2 (fun (j : ℕ) => v j w) (fun (j : ℕ) => U j w) (fun (j : ℕ) => profileJet (f j) w) n

theorem NavierStokes.AxisSourceRegularity.jetLowerTransportSource_ofReal (h b σ X e : ℝ) (v U : ℕ → ℝ) (f : ℕ → Jet2 ℝ) (n : ℕ) : ↑(jetLowerTransportSource h b σ X e v U f n) = jetLowerTransportSource (↑h) (↑b) (↑σ) (↑X) (↑e) (fun (j : ℕ) => ↑(v j)) (fun (j : ℕ) => ↑(U j)) (fun (j : ℕ) => complexifyJet (f j)) n

theorem NavierStokes.AxisSourceRegularity.lowerTransportSource_complex_formula (h b σ : ℝ) (v U f : ℕ → SimilarityProfile.InnerProfile) (n : ℕ) (w : SimilarityProfile.InnerPoint) (hf : ∀ j < n, ContDiffAt ℝ 2 (f j) w) (hL : SimilarityProfile.L h w.2 ≠ 0) : ↑(lowerTransportSource h b σ v U f n w) = jetLowerTransportSource (↑h) (↑b) (↑σ) (↑w.1) (↑w.2) (fun (j : ℕ) => ↑(v j w)) (fun (j : ℕ) => ↑(U j w)) (fun (j : ℕ) => complexifyJet (profileJet (f j) w)) n

theorem NavierStokes.AxisSourceRegularity.jetLowerTransportSource_analytic (h b σ X : ℂ) (v U : ℕ → ℂ → ℂ) (f : ℕ → ℂ → Jet2 ℂ) (n : ℕ) (e : ℂ) (hv : ∀ j < n, AnalyticAt ℂ (v j) e) (hU : ∀ j < n, AnalyticAt ℂ (U j) e) (hf : ∀ j < n, AnalyticJetAt (f j) e) (hL : jetL h e ≠ 0) : AnalyticAt ℂ (fun (z : ℂ) => jetLowerTransportSource h b σ X z (fun (j : ℕ) => v j z) (fun (j : ℕ) => U j z) (fun (j : ℕ) => f j z) n) e

@[reducible, inline]

abbrev NavierStokes.SlowRecursion.Raw : Type

Raw: an abbreviation for ℝ × ℂ → ℂ.

Equations

• NavierStokes.SlowRecursion.Raw = (ℝ × ℂ → ℂ)

structure NavierStokes.SlowRecursion.Regular (R : ℝ) (U : Set ℂ) (F : Raw) : Prop

The induction class for actual scalar radial profiles.

• smooth : ContDiffOn ℝ (↑⊤) F (Set.Ioo (-R) R ×ˢ U)
• holomorphic (r : ℝ) : r ∈ Set.Ioo (-R) R → DifferentiableOn ℂ (fun (z : ℂ) => F (r, z)) U
• even (z : ℂ) : z ∈ U → ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)
• real (r : ℝ) : r ∈ Set.Ioo (-R) R → ∀ (eta : ℝ), ↑eta ∈ U → (F (r, ↑eta)).im = 0

theorem NavierStokes.SlowRecursion.Regular.const (R : ℝ) (U : Set ℂ) (c : ℝ) : Regular R U fun (x : ℝ × ℂ) => ↑c

theorem NavierStokes.SlowRecursion.Regular.add {R : ℝ} {U : Set ℂ} {F G : Raw} (hF : Regular R U F) (hG : Regular R U G) : Regular R U (F + G)

theorem NavierStokes.SlowRecursion.Regular.mul {R : ℝ} {U : Set ℂ} {F G : Raw} (hF : Regular R U F) (hG : Regular R U G) : Regular R U (F * G)

noncomputable def NavierStokes.SlowRecursion.regularAlgebra (R : ℝ) (U : Set ℂ) : Subalgebra ℝ Raw

The class is an actual real algebra of functions.

Equations

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

@[reducible, inline]

abbrev NavierStokes.SlowRecursion.AxisFunction (R : ℝ) (U : Set ℂ) : Type

Axis function: an abbreviation for ↥(regularAlgebra R U) instance {R : ℝ} {U : Set ℂ} : CoeFun (AxisFunction R U) (fun _ => Raw) := ⟨fun F => F.1⟩.

Equations

• NavierStokes.SlowRecursion.AxisFunction R U = ↥(NavierStokes.SlowRecursion.regularAlgebra R U)

@[instance_reducible]

instance NavierStokes.SlowRecursion.instCoeFunAxisFunctionRaw {R : ℝ} {U : Set ℂ} : CoeFun (AxisFunction R U) fun (x : AxisFunction R U) => Raw

Equations

• NavierStokes.SlowRecursion.instCoeFunAxisFunctionRaw = { coe := fun (F : NavierStokes.SlowRecursion.AxisFunction R U) => ↑F }

theorem NavierStokes.SlowRecursion.AxisFunction.smooth {R : ℝ} {U : Set ℂ} (F : AxisFunction R U) : ContDiffOn ℝ (↑⊤) (↑F) (Set.Ioo (-R) R ×ˢ U)

theorem NavierStokes.SlowRecursion.AxisFunction.holomorphic {R : ℝ} {U : Set ℂ} (F : AxisFunction R U) {r : ℝ} (hr : r ∈ Set.Ioo (-R) R) : DifferentiableOn ℂ (fun (z : ℂ) => ↑F (r, z)) U

theorem NavierStokes.SlowRecursion.AxisFunction.even {R : ℝ} {U : Set ℂ} (F : AxisFunction R U) {r : ℝ} (hr : r ∈ Set.Ioo (-R) R) {z : ℂ} (hz : z ∈ U) : ↑F (-r, z) = ↑F (r, z)

theorem NavierStokes.SlowRecursion.AxisFunction.real {R : ℝ} {U : Set ℂ} (F : AxisFunction R U) {r : ℝ} (hr : r ∈ Set.Ioo (-R) R) {eta : ℝ} (heta : ↑eta ∈ U) : (↑F (r, ↑eta)).im = 0

noncomputable def NavierStokes.SlowRecursion.realConstant (R : ℝ) (U : Set ℂ) (c : ℝ) : AxisFunction R U

Real constant, given by algebraMap ℝ (AxisFunction R U) c.

Equations

• NavierStokes.SlowRecursion.realConstant R U c = (algebraMap ℝ (NavierStokes.SlowRecursion.AxisFunction R U)) c

@[simp]

theorem NavierStokes.SlowRecursion.realConstant_apply (R : ℝ) (U : Set ℂ) (c : ℝ) (p : ℝ × ℂ) : ↑(realConstant R U c) p = ↑c

@[simp]

theorem NavierStokes.SlowRecursion.add_apply {R : ℝ} {U : Set ℂ} (F G : AxisFunction R U) (p : ℝ × ℂ) : ↑(F + G) p = ↑F p + ↑G p

@[simp]

theorem NavierStokes.SlowRecursion.mul_apply {R : ℝ} {U : Set ℂ} (F G : AxisFunction R U) (p : ℝ × ℂ) : ↑(F * G) p = ↑F p * ↑G p

@[simp]

theorem NavierStokes.SlowRecursion.sub_apply {R : ℝ} {U : Set ℂ} (F G : AxisFunction R U) (p : ℝ × ℂ) : ↑(F - G) p = ↑F p - ↑G p

@[simp]

theorem NavierStokes.SlowRecursion.neg_apply {R : ℝ} {U : Set ℂ} (F : AxisFunction R U) (p : ℝ × ℂ) : ↑(-F) p = -↑F p

@[simp]

theorem NavierStokes.SlowRecursion.zero_apply {R : ℝ} {U : Set ℂ} (p : ℝ × ℂ) : ↑0 p = 0

@[simp]

theorem NavierStokes.SlowRecursion.one_apply {R : ℝ} {U : Set ℂ} (p : ℝ × ℂ) : ↑1 p = 1

noncomputable def NavierStokes.SlowRecursion.squaredRadius (R : ℝ) (U : Set ℂ) : AxisFunction R U

Squared radius as an element of AxisFunction R U.

Equations

• NavierStokes.SlowRecursion.squaredRadius R U = ⟨fun (p : ℝ × ℂ) => ↑(p.1 ^ 2), ⋯⟩

noncomputable def NavierStokes.SlowRecursion.parameter (R : ℝ) (U : Set ℂ) : AxisFunction R U

Parameter as an element of AxisFunction R U.

Equations

• NavierStokes.SlowRecursion.parameter R U = ⟨Prod.snd, ⋯⟩

theorem NavierStokes.SlowRecursion.interval_mono {R S : ℝ} (hSR : S ≤ R) : Set.Ioo (-S) S ⊆ Set.Ioo (-R) R

noncomputable def NavierStokes.SlowRecursion.restrict {R S : ℝ} {U : Set ℂ} (hSR : S ≤ R) (F : AxisFunction R U) : AxisFunction S U

Restrict as an element of AxisFunction S U.

Equations

• NavierStokes.SlowRecursion.restrict hSR F = ⟨↑F, ⋯⟩

@[simp]

theorem NavierStokes.SlowRecursion.restrict_apply {R S : ℝ} {U : Set ℂ} (hSR : S ≤ R) (F : AxisFunction R U) (p : ℝ × ℂ) : ↑(restrict hSR F) p = ↑F p

noncomputable def NavierStokes.SlowRecursion.inverse {R : ℝ} {U : Set ℂ} (F : AxisFunction R U) (hF : ∀ p ∈ Set.Ioo (-R) R ×ˢ U, ↑F p ≠ 0) : AxisFunction R U

Inverse as an element of AxisFunction R U.

Equations

• NavierStokes.SlowRecursion.inverse F hF = ⟨fun (p : ℝ × ℂ) => (↑F p)⁻¹, ⋯⟩

theorem NavierStokes.SlowRecursion.im_iteratedDeriv_zero {S : Set ℝ} (hS : IsOpen S) {f : ℝ → ℂ} (hf : ContDiffOn ℝ (↑⊤) f S) (hreal : ∀ x ∈ S, (f x).im = 0) {x : ℝ} (hx : x ∈ S) (n : ℕ) : (iteratedDeriv n f x).im = 0

theorem NavierStokes.SlowRecursion.scaled_mem_open {R r t : ℝ} (hr : r ∈ Set.Ioo (-R) R) (ht : t ∈ Set.Icc 0 1) : t * r ∈ Set.Ioo (-R) R

theorem NavierStokes.SlowRecursion.radialJet_one_real {R : ℝ} {U : Set ℂ} (F : AxisFunction R U) {r : ℝ} (hr : r ∈ Set.Ioo (-R) R) {eta : ℝ} (heta : ↑eta ∈ U) : (BoundaryAxisJets.radialJet (↑F) 1 r ↑eta).im = 0

noncomputable def NavierStokes.SlowRecursion.radialDerivative {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) (F : AxisFunction R U) : AxisFunction R U

Radial derivative as an element of AxisFunction R U.

Equations

• NavierStokes.SlowRecursion.radialDerivative hR hU F = ⟨fun (p : ℝ × ℂ) => NavierStokes.BoundaryAxisJets.radialJet (↑F) 1 p.1 p.2, ⋯⟩

theorem NavierStokes.SlowRecursion.parameterDerivative_real {R : ℝ} {U : Set ℂ} (hU : IsOpen U) (F : AxisFunction R U) {r : ℝ} (hr : r ∈ Set.Ioo (-R) R) {eta : ℝ} (heta : ↑eta ∈ U) : (BoundaryAxisJets.complexPartial ↑F (r, ↑eta)).im = 0

noncomputable def NavierStokes.SlowRecursion.parameterDerivative {R : ℝ} {U : Set ℂ} (hU : IsOpen U) (F : AxisFunction R U) : AxisFunction R U

Parameter derivative as an element of AxisFunction R U.

Equations

• NavierStokes.SlowRecursion.parameterDerivative hU F = ⟨NavierStokes.BoundaryAxisJets.complexPartial ↑F, ⋯⟩

theorem NavierStokes.SlowRecursion.hasDerivAt_conjugate {f : ℂ → ℂ} {d z : ℂ} (hf : HasDerivAt f d ((starRingEnd ℂ) z)) : HasDerivAt (fun (w : ℂ) => (starRingEnd ℂ) (f ((starRingEnd ℂ) w))) ((starRingEnd ℂ) d) z

noncomputable def NavierStokes.SlowRecursion.realSymmetrization (F : Raw) (p : ℝ × ℂ) : ℂ

Reflection gives a holomorphic extension of the actual real trace.

Equations

• NavierStokes.SlowRecursion.realSymmetrization F p = (F p + (starRingEnd ℂ) (F (p.1, (starRingEnd ℂ) p.2))) / 2

theorem NavierStokes.SlowRecursion.realSymmetrization_real (F : Raw) (r eta : ℝ) : realSymmetrization F (r, ↑eta) = ↑(F (r, ↑eta)).re

noncomputable def NavierStokes.SlowRecursion.symmetrize {R : ℝ} {U : Set ℂ} (hU : IsOpen U) (hconj : ∀ z ∈ U, (starRingEnd ℂ) z ∈ U) (F : Raw) (hs : ContDiffOn ℝ (↑⊤) F (Set.Ioo (-R) R ×ˢ U)) (hh : ∀ r ∈ Set.Ioo (-R) R, DifferentiableOn ℂ (fun (z : ℂ) => F (r, z)) U) (he : ∀ z ∈ U, ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) : AxisFunction R U

Symmetrize as an element of AxisFunction R U.

Equations

• NavierStokes.SlowRecursion.symmetrize hU hconj F hs hh he = ⟨NavierStokes.SlowRecursion.realSymmetrization F, ⋯⟩

noncomputable def NavierStokes.SlowRecursion.profile {R : ℝ} {U : Set ℂ} (F : AxisFunction R U) (p : ℝ × ℝ) : ℝ

Profile, given by (F (Real.sqrt p.1, (p.2 : ℂ))).re.

Equations

• NavierStokes.SlowRecursion.profile F p = (↑F (√p.1, ↑p.2)).re

noncomputable def NavierStokes.SlowRecursion.complexProfile {R : ℝ} {U : Set ℂ} (F : AxisFunction R U) (p : ℝ × ℂ) : ℂ

Complex profile, given by F (Real.sqrt p.1, p.2).

Equations

• NavierStokes.SlowRecursion.complexProfile F p = ↑F (√p.1, p.2)

theorem NavierStokes.SlowRecursion.sqrt_mem {R X : ℝ} (hR : 0 < R) (hX : X ∈ Set.Ico 0 (R ^ 2)) : √X ∈ Set.Ioo (-R) R

theorem NavierStokes.SlowRecursion.complexProfile_real {R : ℝ} (hR : 0 < R) {U : Set ℂ} (F : AxisFunction R U) {X eta : ℝ} (hX : X ∈ Set.Ico 0 (R ^ 2)) (heta : ↑eta ∈ U) : complexProfile F (X, ↑eta) = ↑(profile F (X, eta))

theorem NavierStokes.SlowRecursion.complexProfile_square {R : ℝ} {U : Set ℂ} (F : AxisFunction R U) {r : ℝ} (hr : r ∈ Set.Ioo (-R) R) {z : ℂ} (hz : z ∈ U) : complexProfile F (r ^ 2, z) = ↑F (r, z)

theorem NavierStokes.SlowRecursion.profile_smooth {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) (F : AxisFunction R U) : ContDiffOn ℝ (↑⊤) (profile F) (Set.Ico 0 (R ^ 2) ×ˢ PositiveAxisExistence.realParameterDomain U)

theorem NavierStokes.SlowRecursion.profile_contDiffAt {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) (F : AxisFunction R U) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) (heta : ↑eta ∈ U) : ContDiffAt ℝ (↑⊤) (profile F) (X, eta)

theorem NavierStokes.SlowRecursion.radialDerivative_value {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) (F : AxisFunction R U) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) (heta : ↑eta ∈ U) : complexProfile (radialDerivative hR hU F) (X, ↑eta) = ↑(SimilarityProfile.partialX (profile F) (X, eta))

theorem NavierStokes.SlowRecursion.parameterDerivative_value {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) (F : AxisFunction R U) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) (heta : ↑eta ∈ U) : complexProfile (parameterDerivative hU F) (X, ↑eta) = ↑(SimilarityProfile.partialEta (profile F) (X, eta))

theorem NavierStokes.SlowRecursion.profile_radialDerivative {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) (F : AxisFunction R U) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) (heta : ↑eta ∈ U) : profile (radialDerivative hR hU F) (X, eta) = SimilarityProfile.partialX (profile F) (X, eta)

theorem NavierStokes.SlowRecursion.profile_parameterDerivative {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) (F : AxisFunction R U) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) (heta : ↑eta ∈ U) : profile (parameterDerivative hU F) (X, eta) = SimilarityProfile.partialEta (profile F) (X, eta)

theorem NavierStokes.SlowRecursion.profile_radialDerivative_germ {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) (F : AxisFunction R U) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) (heta : ↑eta ∈ U) : profile (radialDerivative hR hU F) =ᶠ[nhds (X, eta)] SimilarityProfile.partialX (profile F)

theorem NavierStokes.SlowRecursion.profile_parameterDerivative_germ {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) (F : AxisFunction R U) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) (heta : ↑eta ∈ U) : profile (parameterDerivative hU F) =ᶠ[nhds (X, eta)] SimilarityProfile.partialEta (profile F)

theorem NavierStokes.SlowRecursion.radialDerivative_twice_value {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) (F : AxisFunction R U) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) (heta : ↑eta ∈ U) : complexProfile (radialDerivative hR hU (radialDerivative hR hU F)) (X, ↑eta) = ↑(SimilarityProfile.partialX (SimilarityProfile.partialX (profile F)) (X, eta))

structure NavierStokes.SlowRecursion.Domain (R : ℝ) (U : Set ℂ) (h : ℝ) : Prop

Fixed geometric data for one analytic parameter neighborhood.

• positive : 0 < R
• open_set : IsOpen U
• conjugate (z : ℂ) : z ∈ U → (starRingEnd ℂ) z ∈ U
• denominator (z : ℂ) : z ∈ U → PositiveAxisSystem.ell (↑h) z ≠ 0

theorem NavierStokes.SlowRecursion.Domain.restrict {R S : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (hS : 0 < S) : Domain S U h

noncomputable def NavierStokes.SlowRecursion.denominatorFunction (R : ℝ) (U : Set ℂ) (h : ℝ) : AxisFunction R U

Denominator function, given by 1 - realConstant R U (2 * h) * parameter R U ^ 2.

Equations

• NavierStokes.SlowRecursion.denominatorFunction R U h = 1 - NavierStokes.SlowRecursion.realConstant R U (2 * h) * NavierStokes.SlowRecursion.parameter R U ^ 2

theorem NavierStokes.SlowRecursion.denominatorFunction_apply (R : ℝ) (U : Set ℂ) (h : ℝ) (p : ℝ × ℂ) : ↑(denominatorFunction R U h) p = PositiveAxisSystem.ell (↑h) p.2

noncomputable def NavierStokes.SlowRecursion.inverseDenominator {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) : AxisFunction R U

Inverse denominator, given by inverse (denominatorFunction R U h) (fun p hp => by rw [denominatorFunction_apply] exact c.denominator p.2 hp.2).

Equations

• NavierStokes.SlowRecursion.inverseDenominator c = NavierStokes.SlowRecursion.inverse (NavierStokes.SlowRecursion.denominatorFunction R U h) ⋯

noncomputable def NavierStokes.SlowRecursion.timeOperator {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (b : ℝ) (F : AxisFunction R U) : AxisFunction R U

Time operator as an element of AxisFunction R U.

Equations

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

noncomputable def NavierStokes.SlowRecursion.axialOperator {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (b : ℝ) (F : AxisFunction R U) : AxisFunction R U

Axial operator as an element of AxisFunction R U.

Equations

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

@[simp]

theorem NavierStokes.SlowRecursion.complexProfile_add {R : ℝ} {U : Set ℂ} (F G : AxisFunction R U) (p : ℝ × ℂ) : complexProfile (F + G) p = complexProfile F p + complexProfile G p

@[simp]

theorem NavierStokes.SlowRecursion.complexProfile_sub {R : ℝ} {U : Set ℂ} (F G : AxisFunction R U) (p : ℝ × ℂ) : complexProfile (F - G) p = complexProfile F p - complexProfile G p

@[simp]

theorem NavierStokes.SlowRecursion.complexProfile_mul {R : ℝ} {U : Set ℂ} (F G : AxisFunction R U) (p : ℝ × ℂ) : complexProfile (F * G) p = complexProfile F p * complexProfile G p

@[simp]

theorem NavierStokes.SlowRecursion.complexProfile_neg {R : ℝ} {U : Set ℂ} (F : AxisFunction R U) (p : ℝ × ℂ) : complexProfile (-F) p = -complexProfile F p

@[simp]

theorem NavierStokes.SlowRecursion.complexProfile_pow {R : ℝ} {U : Set ℂ} (F : AxisFunction R U) (k : ℕ) (p : ℝ × ℂ) : complexProfile (F ^ k) p = complexProfile F p ^ k

@[simp]

theorem NavierStokes.SlowRecursion.complexProfile_zero {R : ℝ} {U : Set ℂ} (p : ℝ × ℂ) : complexProfile 0 p = 0

@[simp]

theorem NavierStokes.SlowRecursion.complexProfile_one {R : ℝ} {U : Set ℂ} (p : ℝ × ℂ) : complexProfile 1 p = 1

@[simp]

theorem NavierStokes.SlowRecursion.complexProfile_realConstant (R : ℝ) (U : Set ℂ) (b : ℝ) (p : ℝ × ℂ) : complexProfile (realConstant R U b) p = ↑b

@[simp]

theorem NavierStokes.SlowRecursion.complexProfile_parameter (R : ℝ) (U : Set ℂ) (p : ℝ × ℂ) : complexProfile (parameter R U) p = p.2

@[simp]

theorem NavierStokes.SlowRecursion.complexProfile_squaredRadius (R : ℝ) (U : Set ℂ) {X : ℝ} (hX : 0 ≤ X) (z : ℂ) : complexProfile (squaredRadius R U) (X, z) = ↑X

@[simp]

theorem NavierStokes.SlowRecursion.complexProfile_inverseDenominator {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (p : ℝ × ℂ) : complexProfile (inverseDenominator c) p = (PositiveAxisSystem.ell (↑h) p.2)⁻¹

theorem NavierStokes.SlowRecursion.timeOperator_value {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (b : ℝ) (F : AxisFunction R U) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) (heta : ↑eta ∈ U) : complexProfile (timeOperator c b F) (X, ↑eta) = ↑(SimilarityProfile.T h b (profile F) (X, eta))

theorem NavierStokes.SlowRecursion.axialOperator_value {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (b : ℝ) (F : AxisFunction R U) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) (heta : ↑eta ∈ U) : complexProfile (axialOperator c b F) (X, ↑eta) = ↑(SimilarityProfile.Z h b (profile F) (X, eta))

theorem NavierStokes.SlowRecursion.axialOperator_germ {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (b : ℝ) (F : AxisFunction R U) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) (heta : ↑eta ∈ U) : profile (axialOperator c b F) =ᶠ[nhds (X, eta)] SimilarityProfile.Z h b (profile F)

theorem NavierStokes.SlowRecursion.axialOperator_twice_value {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (b₁ b₂ : ℝ) (F : AxisFunction R U) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) (heta : ↑eta ∈ U) : complexProfile (axialOperator c b₂ (axialOperator c b₁ F)) (X, ↑eta) = ↑(SimilarityProfile.Z h b₂ (SimilarityProfile.Z h b₁ (profile F)) (X, eta))

@[simp]

theorem NavierStokes.SlowRecursion.complexProfile_sum {ι : Type u_1} {R : ℝ} {U : Set ℂ} (s : Finset ι) (F : ι → AxisFunction R U) (p : ℝ × ℂ) : complexProfile (∑ i ∈ s, F i) p = ∑ i ∈ s, complexProfile (F i) p

noncomputable def NavierStokes.SlowRecursion.priorDiffusion {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (b : ℝ) (F : ℕ → AxisFunction R U) (n : ℕ) : AxisFunction R U

Prior diffusion, with branches according to n = 0.

Equations

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

theorem NavierStokes.SlowRecursion.priorDiffusion_value {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (b : ℝ) (F : ℕ → AxisFunction R U) (n : ℕ) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) (heta : ↑eta ∈ U) : complexProfile (priorDiffusion c b F n) (X, ↑eta) = ↑(PositiveAxisSystem.precedingDiffusion h b (fun (j : ℕ) => profile (F j)) n (X, eta))

noncomputable def NavierStokes.SlowRecursion.shiftedBetaDiffusion {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (F : ℕ → AxisFunction R U) : ℕ → AxisFunction R U

Shifted beta diffusion used in slow recursion.

Equations

• One or more equations did not get rendered due to their size.
• NavierStokes.SlowRecursion.shiftedBetaDiffusion c F 0 = 0

theorem NavierStokes.SlowRecursion.shiftedBetaDiffusion_value {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (F : ℕ → AxisFunction R U) (k : ℕ) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) (heta : ↑eta ∈ U) : complexProfile (shiftedBetaDiffusion c F k) (X, ↑eta) = ↑(AxisSourceRegularity.shiftedAxialFactor h (fun (j : ℕ) => profile (F j)) k (X, eta))

noncomputable def NavierStokes.SlowRecursion.radialSource {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (u beta : ℕ → AxisFunction R U) (k : ℕ) : AxisFunction R U

Radial source, constructed using timeOperator.

Equations

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

theorem NavierStokes.SlowRecursion.radialSource_value {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (u beta : ℕ → AxisFunction R U) (k : ℕ) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) (heta : ↑eta ∈ U) : complexProfile (radialSource c u beta k) (X, ↑eta) = ↑(AxisSourceRegularity.omegaDivX h (fun (j : ℕ) => profile (u j)) (fun (j : ℕ) => profile (beta j)) k (X, eta))

noncomputable def NavierStokes.SlowRecursion.previousRadialSource {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (u beta : ℕ → AxisFunction R U) : ℕ → AxisFunction R U

Previous radial source as an element of ℕ → AxisFunction R U | 0 => 0 | k + 1 => radialSource c u beta k.

Equations

• NavierStokes.SlowRecursion.previousRadialSource c u beta 0 = 0
• NavierStokes.SlowRecursion.previousRadialSource c u beta k.succ = NavierStokes.SlowRecursion.radialSource c u beta k

theorem NavierStokes.SlowRecursion.previousRadialSource_value {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (u beta : ℕ → AxisFunction R U) (n : ℕ) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) (heta : ↑eta ∈ U) : complexProfile (previousRadialSource c u beta n) (X, ↑eta) = ↑(AxisSourceRegularity.previousOmegaDivX h (fun (j : ℕ) => profile (u j)) (fun (j : ℕ) => profile (beta j)) n (X, eta))

noncomputable def NavierStokes.SlowRecursion.angularSource {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (phi u beta : ℕ → AxisFunction R U) (n : ℕ) : AxisFunction R U

Angular source as an element of AxisFunction R U.

Equations

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

noncomputable def NavierStokes.SlowRecursion.axialSource {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (u beta : ℕ → AxisFunction R U) (n : ℕ) : AxisFunction R U

Axial source as an element of AxisFunction R U.

Equations

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

noncomputable def NavierStokes.SlowRecursion.pressureProduct {R : ℝ} {U : Set ℂ} (phi : ℕ → AxisFunction R U) (n : ℕ) : AxisFunction R U

Pressure product, given by ∑ i ∈ Finset.range (n - 1), phi (i + 1) * phi (n - (i + 1)).

Equations

• NavierStokes.SlowRecursion.pressureProduct phi n = ∑ i ∈ Finset.range (n - 1), phi (i + 1) * phi (n - (i + 1))

noncomputable def NavierStokes.SlowRecursion.sourceFunctions {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (phi u beta : ℕ → AxisFunction R U) (n : ℕ) : Fin 11 → AxisFunction R U

Each of the eleven inputs is an actual member of the smooth function algebra; their regularity follows by construction from the lower profiles.

Equations

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

noncomputable def NavierStokes.SlowRecursion.sourceData {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (phi u beta : ℕ → AxisFunction R U) (n : ℕ) : PositiveAxisSystem.CoefficientData

Source data, defined pointwise by complexProfile (sourceFunctions c phi u beta n i).

Equations

• NavierStokes.SlowRecursion.sourceData c phi u beta n i = NavierStokes.SlowRecursion.complexProfile (NavierStokes.SlowRecursion.sourceFunctions c phi u beta n i)

theorem NavierStokes.SlowRecursion.sourceData_regular {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (phi u beta : ℕ → AxisFunction R U) (n : ℕ) : PositiveAxisExistence.LowerInputRegularity R U (↑h) (sourceData c phi u beta n)

theorem NavierStokes.SlowRecursion.sourceData_real {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (phi u beta : ℕ → AxisFunction R U) (n : ℕ) : PositiveAxisExistence.RealCompatible R U (sourceData c phi u beta n) (PositiveAxisExistence.lowerHistoryData h n (fun (j : ℕ) => profile (phi j)) (fun (j : ℕ) => profile (u j)) (fun (j : ℕ) => profile (beta j)) (AxisSourceRegularity.previousOmegaDivX h (fun (j : ℕ) => profile (u j)) (fun (j : ℕ) => profile (beta j)) n))

noncomputable def NavierStokes.SlowRecursion.betaOperator {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (n : ℕ) (u k : AxisFunction R U) : AxisFunction R U

Beta operator as an element of AxisFunction R U.

Equations

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

theorem NavierStokes.SlowRecursion.betaOperator_value {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (n : ℕ) (u k : AxisFunction R U) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) (heta : ↑eta ∈ U) : complexProfile (betaOperator c n u k) (X, ↑eta) = ↑(PositiveAxisExistence.newBeta h n (profile u) (profile k) (X, eta))

@[reducible, inline]

abbrev NavierStokes.SlowRecursion.Coefficient (R : ℝ) (U : Set ℂ) : Type

Coefficient: an abbreviation for Fin 5 → AxisFunction R U.

Equations

• NavierStokes.SlowRecursion.Coefficient R U = (Fin 5 → NavierStokes.SlowRecursion.AxisFunction R U)

noncomputable def NavierStokes.SlowRecursion.stepRaw {R S : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (hS : 0 < S) (C : ℝ) (n : ℕ) (F : ℕ → Coefficient R U) : VolterraAnalyticBounds.Field

Step raw, constructed using PositiveAxisExistence.positiveSolution.

Equations

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

noncomputable def NavierStokes.SlowRecursion.stepComponent {R S : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (hS : 0 < S) (hSR : S < R) (C : ℝ) (n : ℕ) (F : ℕ → Coefficient R U) (i : Fin 6) (hi : ↑i < 4) : AxisFunction S U

Step component as an element of AxisFunction S U.

Equations

• NavierStokes.SlowRecursion.stepComponent c hS hSR C n F i hi = NavierStokes.SlowRecursion.symmetrize ⋯ ⋯ (fun (p : ℝ × ℂ) => NavierStokes.SlowRecursion.stepRaw c hS C n F p.1 p.2 i) ⋯ ⋯ ⋯

theorem NavierStokes.SlowRecursion.stepComponent_profile {R S : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (hS : 0 < S) (hSR : S < R) (C : ℝ) (n : ℕ) (F : ℕ → Coefficient R U) (i : Fin 6) (hi : ↑i < 4) : profile (stepComponent c hS hSR C n F i hi) = PositiveAxisExistence.xProfile (stepRaw c hS C n F) i

theorem NavierStokes.SlowRecursion.stepComponent_axis_zero {R S : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (hS : 0 < S) (hSR : S < R) (C : ℝ) (n : ℕ) (F : ℕ → Coefficient R U) (i : Fin 6) (hi : ↑i < 4) {z : ℂ} (hz : z ∈ U) : ↑(stepComponent c hS hSR C n F i hi) (0, z) = 0

noncomputable def NavierStokes.SlowRecursion.step {R S : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (hS : 0 < S) (hSR : S < R) (C : ℝ) (n : ℕ) (F : ℕ → Coefficient R U) : Coefficient S U

One actual inductive step. The first four profiles come from the convergent Volterra solution; the fifth is the genuine divergence formula.

Equations

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

theorem NavierStokes.SlowRecursion.step_profile {R S : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (hS : 0 < S) (hSR : S < R) (C : ℝ) (n : ℕ) (F : ℕ → Coefficient R U) (i : Fin 4) : profile (step c hS hSR C n F ⟨↑i, ⋯⟩) = PositiveAxisExistence.xProfile (stepRaw c hS C n F) ⟨↑i, ⋯⟩

theorem NavierStokes.SlowRecursion.sourceData_real_smaller {R S : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (hS : 0 < S) (hSR : S ≤ R) (phi u beta : ℕ → AxisFunction R U) (n : ℕ) : PositiveAxisExistence.RealCompatible S U (sourceData c phi u beta n) (PositiveAxisExistence.lowerHistoryData h n (fun (j : ℕ) => profile (phi j)) (fun (j : ℕ) => profile (u j)) (fun (j : ℕ) => profile (beta j)) (AxisSourceRegularity.previousOmegaDivX h (fun (j : ℕ) => profile (u j)) (fun (j : ℕ) => profile (beta j)) n))

theorem NavierStokes.SlowRecursion.step_beta {R S : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (hS : 0 < S) (hSR : S < R) (C : ℝ) (n : ℕ) (F : ℕ → Coefficient R U) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (S ^ 2)) (heta : ↑eta ∈ U) : profile (step c hS hSR C n F 4) (X, eta) = PositiveAxisExistence.newBeta h n (profile (step c hS hSR C n F 1)) (profile (step c hS hSR C n F 2)) (X, eta)

theorem NavierStokes.SlowRecursion.step_expanded {R S : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (hS : 0 < S) (hSR : S < R) (C : ℝ) (n : ℕ) (F : ℕ → Coefficient R U) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (S ^ 2)) (heta : ↑eta ∈ U) : PositiveAxisSystem.ExpandedEquations h (PositiveAxisSystem.slowPower h n) C eta X (PositiveAxisSystem.baseAtOrderZero (fun (j : ℕ) => PositiveAxisSystem.actualJet (profile (F j 0)) (X, eta)) (fun (j : ℕ) => PositiveAxisSystem.actualJet (profile (F j 1)) (X, eta)) fun (j : ℕ) => profile (F j 4) (X, eta)) (PositiveAxisSystem.actualLowerSource h n (fun (j : ℕ) => profile (F j 0)) (fun (j : ℕ) => profile (F j 1)) (fun (j : ℕ) => profile (F j 4)) (AxisSourceRegularity.previousOmegaDivX h (fun (j : ℕ) => profile (F j 1)) (fun (j : ℕ) => profile (F j 4)) n) (X, eta)) (PositiveAxisSystem.actualJet (profile (step c hS hSR C n F 0)) (X, eta)) (PositiveAxisSystem.actualJet (profile (step c hS hSR C n F 1)) (X, eta)) (PositiveAxisSystem.actualJet (profile (step c hS hSR C n F 2)) (X, eta)) (PositiveAxisSystem.actualJet (profile (step c hS hSR C n F 3)) (X, eta))

theorem NavierStokes.SlowRecursion.betaOperator_axis_zero {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (n : ℕ) (u k : AxisFunction R U) (hu : ∀ z ∈ U, ↑u (0, z) = 0) (hk : ∀ z ∈ U, ↑k (0, z) = 0) {z : ℂ} (hz : z ∈ U) : ↑(betaOperator c n u k) (0, z) = 0

theorem NavierStokes.SlowRecursion.step_axis_zero {R S : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (hS : 0 < S) (hSR : S < R) (C : ℝ) (n : ℕ) (F : ℕ → Coefficient R U) (i : Fin 5) {z : ℂ} (hz : z ∈ U) : ↑(step c hS hSR C n F i) (0, z) = 0

noncomputable def NavierStokes.SlowRecursion.radius (core buffer : ℝ) (n : ℕ) : ℝ

Buffer radii approach a fixed positive core without ever reaching it.

Equations

• NavierStokes.SlowRecursion.radius core buffer n = core + buffer / (↑n + 1)

theorem NavierStokes.SlowRecursion.core_lt_radius {core buffer : ℝ} (hbuffer : 0 < buffer) (n : ℕ) : core < radius core buffer n

theorem NavierStokes.SlowRecursion.radius_pos {core buffer : ℝ} (hcore : 0 < core) (hbuffer : 0 < buffer) (n : ℕ) : 0 < radius core buffer n

theorem NavierStokes.SlowRecursion.radius_antitone {core buffer : ℝ} (hbuffer : 0 ≤ buffer) : Antitone (radius core buffer)

theorem NavierStokes.SlowRecursion.radius_succ_lt {core buffer : ℝ} (hbuffer : 0 < buffer) (n : ℕ) : radius core buffer (n + 1) < radius core buffer n

theorem NavierStokes.SlowRecursion.radiusDomain {core buffer : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain (radius core buffer 0) U h) (hcore : 0 < core) (hbuffer : 0 < buffer) (n : ℕ) : Domain (radius core buffer n) U h

noncomputable def NavierStokes.SlowRecursion.lowerHistory {core buffer : ℝ} {U : Set ℂ} (hbuffer : 0 < buffer) (n : ℕ) (previous : (j : ℕ) → j < n → Coefficient (radius core buffer j) U) : ℕ → Coefficient (radius core buffer (n - 1)) U

Only coefficients with index below n are accessed. The zero branch is outside every finite source sum and is not an assumed future coefficient.

Equations

• NavierStokes.SlowRecursion.lowerHistory hbuffer n previous j = if hj : j < n then fun (i : Fin 5) => NavierStokes.SlowRecursion.restrict ⋯ (previous j hj i) else 0

theorem NavierStokes.SlowRecursion.lowerHistory_apply {core buffer : ℝ} {U : Set ℂ} (hbuffer : 0 < buffer) (n : ℕ) (previous : (j : ℕ) → j < n → Coefficient (radius core buffer j) U) {j : ℕ} (hj : j < n) (i : Fin 5) (p : ℝ × ℂ) : ↑(lowerHistory hbuffer n previous j i) p = ↑(previous j hj i) p

noncomputable def NavierStokes.SlowRecursion.recursionStep {core buffer : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain (radius core buffer 0) U h) (hcore : 0 < core) (hbuffer : 0 < buffer) (C : ℝ) (base : Coefficient (radius core buffer 0) U) (n : ℕ) : ((j : ℕ) → j < n → Coefficient (radius core buffer j) U) → Coefficient (radius core buffer n) U

Recursion step used in slow recursion.

Equations

• NavierStokes.SlowRecursion.recursionStep c hcore hbuffer C base 0 x_2 = base
• NavierStokes.SlowRecursion.recursionStep c hcore hbuffer C base n.succ previous = NavierStokes.SlowRecursion.step ⋯ ⋯ ⋯ C (n + 1) (NavierStokes.SlowRecursion.lowerHistory hbuffer (n + 1) previous)

noncomputable def NavierStokes.SlowRecursion.hierarchy {core buffer : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain (radius core buffer 0) U h) (hcore : 0 < core) (hbuffer : 0 < buffer) (C : ℝ) (base : Coefficient (radius core buffer 0) U) (n : ℕ) : Coefficient (radius core buffer n) U

The actual sequence is built by well-founded recursion from one base coefficient. Every recursive input has a strictly smaller slow index.

Equations

• NavierStokes.SlowRecursion.hierarchy c hcore hbuffer C base n = ⋯.fix (NavierStokes.SlowRecursion.recursionStep c hcore hbuffer C base) n

theorem NavierStokes.SlowRecursion.hierarchy_zero {core buffer : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain (radius core buffer 0) U h) (hcore : 0 < core) (hbuffer : 0 < buffer) (C : ℝ) (base : Coefficient (radius core buffer 0) U) : hierarchy c hcore hbuffer C base 0 = base

theorem NavierStokes.SlowRecursion.hierarchy_succ {core buffer : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain (radius core buffer 0) U h) (hcore : 0 < core) (hbuffer : 0 < buffer) (C : ℝ) (base : Coefficient (radius core buffer 0) U) (n : ℕ) : hierarchy c hcore hbuffer C base (n + 1) = step ⋯ ⋯ ⋯ C (n + 1) (lowerHistory hbuffer (n + 1) fun (j : ℕ) (x : j < n + 1) => hierarchy c hcore hbuffer C base j)

noncomputable def NavierStokes.SlowRecursion.sequence {core buffer : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain (radius core buffer 0) U h) (hcore : 0 < core) (hbuffer : 0 < buffer) (C : ℝ) (base : Coefficient (radius core buffer 0) U) (n : ℕ) : Coefficient core U

All orders on the same radial rectangle and the same complex parameter neighborhood. Restriction changes no pointwise function value.

Equations

• NavierStokes.SlowRecursion.sequence c hcore hbuffer C base n i = NavierStokes.SlowRecursion.restrict ⋯ (NavierStokes.SlowRecursion.hierarchy c hcore hbuffer C base n i)

theorem NavierStokes.SlowRecursion.sequence_profile {core buffer : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain (radius core buffer 0) U h) (hcore : 0 < core) (hbuffer : 0 < buffer) (C : ℝ) (base : Coefficient (radius core buffer 0) U) (n : ℕ) (i : Fin 5) : profile (sequence c hcore hbuffer C base n i) = profile (hierarchy c hcore hbuffer C base n i)

theorem NavierStokes.SlowRecursion.sequence_zero {core buffer : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain (radius core buffer 0) U h) (hcore : 0 < core) (hbuffer : 0 < buffer) (C : ℝ) (base : Coefficient (radius core buffer 0) U) (i : Fin 5) : profile (sequence c hcore hbuffer C base 0 i) = profile (base i)

theorem NavierStokes.SlowRecursion.lowerHistory_profile {core buffer : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain (radius core buffer 0) U h) (hcore : 0 < core) (hbuffer : 0 < buffer) (C : ℝ) (base : Coefficient (radius core buffer 0) U) {n j : ℕ} (hj : j < n) (i : Fin 5) : profile (lowerHistory hbuffer n (fun (j : ℕ) (x : j < n) => hierarchy c hcore hbuffer C base j) j i) = profile (sequence c hcore hbuffer C base j i)

theorem NavierStokes.SlowRecursion.previousOmega_congr (h : ℝ) {n : ℕ} {u beta u' beta' : ℕ → SimilarityProfile.InnerProfile} (hu : ∀ j < n, u j = u' j) (hb : ∀ j < n, beta j = beta' j) : AxisSourceRegularity.previousOmegaDivX h u beta n = AxisSourceRegularity.previousOmegaDivX h u' beta' n

theorem NavierStokes.SlowRecursion.sequence_succ_profile {core buffer : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain (radius core buffer 0) U h) (hcore : 0 < core) (hbuffer : 0 < buffer) (C : ℝ) (base : Coefficient (radius core buffer 0) U) (n : ℕ) (i : Fin 5) : profile (sequence c hcore hbuffer C base (n + 1) i) = profile (step ⋯ ⋯ ⋯ C (n + 1) (lowerHistory hbuffer (n + 1) fun (j : ℕ) (x : j < n + 1) => hierarchy c hcore hbuffer C base j) i)

theorem NavierStokes.SlowRecursion.core_square_lt {core buffer X : ℝ} (hcore : 0 < core) (hbuffer : 0 < buffer) (hX : X < core ^ 2) (n : ℕ) : X < radius core buffer n ^ 2

theorem NavierStokes.SlowRecursion.sequence_beta {core buffer : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain (radius core buffer 0) U h) (hcore : 0 < core) (hbuffer : 0 < buffer) (C : ℝ) (base : Coefficient (radius core buffer 0) U) {n : ℕ} (hn : 0 < n) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (core ^ 2)) (heta : ↑eta ∈ U) : profile (sequence c hcore hbuffer C base n 4) (X, eta) = PositiveAxisExistence.newBeta h n (profile (sequence c hcore hbuffer C base n 1)) (profile (sequence c hcore hbuffer C base n 2)) (X, eta)

theorem NavierStokes.SlowRecursion.sequence_expanded {core buffer : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain (radius core buffer 0) U h) (hcore : 0 < core) (hbuffer : 0 < buffer) (C : ℝ) (base : Coefficient (radius core buffer 0) U) {n : ℕ} (hn : 0 < n) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (core ^ 2)) (heta : ↑eta ∈ U) : have A := sequence c hcore hbuffer C base; PositiveAxisSystem.ExpandedEquations h (PositiveAxisSystem.slowPower h n) C eta X (PositiveAxisSystem.baseAtOrderZero (fun (j : ℕ) => PositiveAxisSystem.actualJet (profile (A j 0)) (X, eta)) (fun (j : ℕ) => PositiveAxisSystem.actualJet (profile (A j 1)) (X, eta)) fun (j : ℕ) => profile (A j 4) (X, eta)) (PositiveAxisSystem.actualLowerSource h n (fun (j : ℕ) => profile (A j 0)) (fun (j : ℕ) => profile (A j 1)) (fun (j : ℕ) => profile (A j 4)) (AxisSourceRegularity.previousOmegaDivX h (fun (j : ℕ) => profile (A j 1)) (fun (j : ℕ) => profile (A j 4)) n) (X, eta)) (PositiveAxisSystem.actualJet (profile (A n 0)) (X, eta)) (PositiveAxisSystem.actualJet (profile (A n 1)) (X, eta)) (PositiveAxisSystem.actualJet (profile (A n 2)) (X, eta)) (PositiveAxisSystem.actualJet (profile (A n 3)) (X, eta))

theorem NavierStokes.SlowRecursion.sequence_positive_order {core buffer : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain (radius core buffer 0) U h) (hcore : 0 < core) (hbuffer : 0 < buffer) (C : ℝ) (base : Coefficient (radius core buffer 0) U) {n : ℕ} (hn : 0 < n) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (core ^ 2)) (heta : ↑eta ∈ U) : have A := sequence c hcore hbuffer C base; PositiveAxisSystem.PositiveOrderEquations h C eta X n (fun (j : ℕ) => PositiveAxisSystem.actualJet (profile (A j 0)) (X, eta)) (fun (j : ℕ) => PositiveAxisSystem.actualJet (profile (A j 1)) (X, eta)) (fun (j : ℕ) => profile (A j 4) (X, eta)) (PositiveAxisSystem.actualJet (profile (A n 2)) (X, eta)) (PositiveAxisSystem.actualJet (profile (A n 3)) (X, eta)) (PositiveAxisSystem.precedingDiffusion h (PositiveAxisSystem.angularPower h) (fun (j : ℕ) => profile (A j 0)) n (X, eta)) (PositiveAxisSystem.precedingDiffusion h (PositiveAxisSystem.axialPower h) (fun (j : ℕ) => profile (A j 1)) n (X, eta)) (AxisSourceRegularity.previousOmegaDivX h (fun (j : ℕ) => profile (A j 1)) (fun (j : ℕ) => profile (A j 4)) n (X, eta))

Every positive slow coefficient solves the actual finite convolution equations, with the lower radial residual computed from the same hierarchy.

theorem NavierStokes.SlowRecursion.sequence_axis_zero {core buffer : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain (radius core buffer 0) U h) (hcore : 0 < core) (hbuffer : 0 < buffer) (C : ℝ) (base : Coefficient (radius core buffer 0) U) {n : ℕ} (hn : 0 < n) (i : Fin 5) {z : ℂ} (hz : z ∈ U) : ↑(sequence c hcore hbuffer C base n i) (0, z) = 0

theorem NavierStokes.SlowRecursion.domain_real_denominator {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) {eta : ℝ} (heta : ↑eta ∈ U) : SimilarityProfile.L h eta ≠ 0

theorem NavierStokes.SlowRecursion.sequence_omega_quotient {core buffer : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain (radius core buffer 0) U h) (hcore : 0 < core) (hbuffer : 0 < buffer) (C : ℝ) (base : Coefficient (radius core buffer 0) U) (k : ℕ) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (core ^ 2)) (heta : ↑eta ∈ U) : have A := sequence c hcore hbuffer C base; AxisSourceRegularity.omega h (fun (j : ℕ) => profile (A j 1)) (fun (j : ℕ) => AxisSourceRegularity.axisFactor (profile (A j 4))) k (X, eta) / X = AxisSourceRegularity.previousOmegaDivX h (fun (j : ℕ) => profile (A j 1)) (fun (j : ℕ) => profile (A j 4)) (k + 1) (X, eta)

The supplied regular representative really is the original radial residual divided by X, for every previously constructed order.

theorem NavierStokes.SlowRecursion.average_from_equation {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) (u k : AxisFunction R U) {eta X : ℝ} (heta : ↑eta ∈ U) (hX : X ∈ Set.Ioo 0 (R ^ 2)) (heq : ∀ Y ∈ Set.Ioo 0 (R ^ 2), Y * (SimilarityProfile.partialX (profile u) (Y, eta) + SimilarityProfile.partialX (profile k) (Y, eta)) + profile k (Y, eta) = 0) : ProfileHistories.average (profile u) (X, eta) = profile u (X, eta) + profile k (X, eta)

theorem NavierStokes.SlowRecursion.sequence_average {core buffer : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain (radius core buffer 0) U h) (hcore : 0 < core) (hbuffer : 0 < buffer) (C : ℝ) (base : Coefficient (radius core buffer 0) U) {n : ℕ} (hn : 0 < n) {X eta : ℝ} (hX : X ∈ Set.Ico 0 (core ^ 2)) (heta : ↑eta ∈ U) : have A := sequence c hcore hbuffer C base; ProfileHistories.average (profile (A n 1)) (X, eta) = profile (A n 1) (X, eta) + profile (A n 2) (X, eta)

The stored average defect is the literal integral average, including the axis. No free integration constant survives the regular zero trace.

theorem NavierStokes.SlowRecursion.profile_axis_jet {R : ℝ} (hR : 0 < R) {U : Set ℂ} (F : AxisFunction R U) {eta : ℝ} (heta : ↑eta ∈ U) (k : ℕ) : iteratedDerivWithin k (fun (X : ℝ) => profile F (X, eta)) (Set.Ici 0) 0 = (↑k.factorial / ↑(2 * k).factorial) • iteratedDeriv (2 * k) (fun (r : ℝ) => (↑F (r, ↑eta)).re) 0

noncomputable def NavierStokes.SlowRecursion.makeBase {R : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain R U h) (phi u average pressure : AxisFunction R U) : Coefficient R U

A base made from four genuine profiles; its divergence coefficient is computed by the same canonical derivative operator used in the recursion.

Equations

• NavierStokes.SlowRecursion.makeBase c phi u average pressure = ![phi, u, average - u, pressure, NavierStokes.SlowRecursion.betaOperator c 0 u (average - u)]

theorem NavierStokes.SlowRecursion.sequence_smooth {core buffer : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain (radius core buffer 0) U h) (hcore : 0 < core) (hbuffer : 0 < buffer) (C : ℝ) (base : Coefficient (radius core buffer 0) U) (n : ℕ) (i : Fin 5) : ContDiffOn ℝ (↑⊤) (profile (sequence c hcore hbuffer C base n i)) (Set.Ico 0 (core ^ 2) ×ˢ PositiveAxisExistence.realParameterDomain U)

theorem NavierStokes.SlowRecursion.sequence_mixed_pullback_smooth {core buffer : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain (radius core buffer 0) U h) (hcore : 0 < core) (hbuffer : 0 < buffer) (C : ℝ) (base : Coefficient (radius core buffer 0) U) (n : ℕ) (i : Fin 5) (k m : ℕ) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => BoundaryAxisJets.mixedAxisJet (↑(sequence c hcore hbuffer C base n i)) k m (p.1 ^ 2, p.2)) (Set.Ioo (-core) core ×ˢ U)

theorem NavierStokes.SlowRecursion.sequence_mixed_pullback_holomorphic {core buffer : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain (radius core buffer 0) U h) (hcore : 0 < core) (hbuffer : 0 < buffer) (C : ℝ) (base : Coefficient (radius core buffer 0) U) (n : ℕ) (i : Fin 5) (k m : ℕ) {r : ℝ} (hr : r ∈ Set.Ioo (-core) core) : DifferentiableOn ℂ (fun (z : ℂ) => BoundaryAxisJets.mixedAxisJet (↑(sequence c hcore hbuffer C base n i)) k m (r ^ 2, z)) U

def NavierStokes.SlowRecursion.OrderEquations {R : ℝ} {U : Set ℂ} (h C : ℝ) (A : ℕ → Coefficient R U) (n : ℕ) (w : SimilarityProfile.InnerPoint) : Prop

The concrete finite equations of an actual sequence of profile functions.

Equations

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

structure NavierStokes.SlowRecursion.LocalHierarchy (R : ℝ) (U : Set ℂ) (h C : ℝ) (base : Fin 5 → SimilarityProfile.InnerProfile) : Type

A local slow hierarchy is the output, not a hypothesis on the data. Its underlying type supplies genuine compatible smooth coefficient functions.

• coefficients : ℕ → Coefficient R U

  Coefficients of LocalHierarchy, of type ℕ → Coefficient R U.

• starts (i : Fin 5) : profile (self.coefficients 0 i) = base i
• zero_axis (n : ℕ) : 0 < n → ∀ (i : Fin 5), ∀ z ∈ U, ↑(self.coefficients n i) (0, z) = 0
• beta (n : ℕ) : 0 < n → ∀ X ∈ Set.Ioo 0 (R ^ 2), ∀ (eta : ℝ), ↑eta ∈ U → profile (self.coefficients n 4) (X, eta) = PositiveAxisExistence.newBeta h n (profile (self.coefficients n 1)) (profile (self.coefficients n 2)) (X, eta)
• equations (n : ℕ) : 0 < n → ∀ X ∈ Set.Ioo 0 (R ^ 2), ∀ (eta : ℝ), ↑eta ∈ U → OrderEquations h C self.coefficients n (X, eta)
• average (n : ℕ) : 0 < n → ∀ X ∈ Set.Ico 0 (R ^ 2), ∀ (eta : ℝ), ↑eta ∈ U → ProfileHistories.average (profile (self.coefficients n 1)) (X, eta) = profile (self.coefficients n 1) (X, eta) + profile (self.coefficients n 2) (X, eta)

noncomputable def NavierStokes.SlowRecursion.buildLocalHierarchy {core buffer : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain (radius core buffer 0) U h) (hcore : 0 < core) (hbuffer : 0 < buffer) (C : ℝ) (base : Coefficient (radius core buffer 0) U) : LocalHierarchy core U h C fun (i : Fin 5) => profile (base i)

Construct every positive slow order from a single finite base profile. The entire sequence uses one fixed radial core and one fixed parameter domain.

Equations

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

theorem NavierStokes.SlowRecursion.exists_local_slow_hierarchy {core buffer : ℝ} {U : Set ℂ} {h : ℝ} (c : Domain (radius core buffer 0) U h) (hcore : 0 < core) (hbuffer : 0 < buffer) (C : ℝ) (base : Coefficient (radius core buffer 0) U) : Nonempty (LocalHierarchy core U h C fun (i : Fin 5) => profile (base i))

theorem NavierStokes.SlowRecursion.LocalHierarchy.profiles_smooth {R : ℝ} {U : Set ℂ} {h C : ℝ} {base : Fin 5 → SimilarityProfile.InnerProfile} (A : LocalHierarchy R U h C base) (hR : 0 < R) (hU : IsOpen U) (n : ℕ) (i : Fin 5) : ContDiffOn ℝ (↑⊤) (profile (A.coefficients n i)) (Set.Ico 0 (R ^ 2) ×ˢ PositiveAxisExistence.realParameterDomain U)

theorem NavierStokes.SlowRecursion.LocalHierarchy.equations_on_window {R : ℝ} {U : Set ℂ} {h C a b : ℝ} {base : Fin 5 → SimilarityProfile.InnerProfile} (A : LocalHierarchy R U h C base) (hwindow : ∀ eta ∈ Set.Icc a b, ↑eta ∈ U) {n : ℕ} (hn : 0 < n) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) (heta : eta ∈ Set.Icc a b) : OrderEquations h C A.coefficients n (X, eta)

Any fixed real parameter window contained in the input neighborhood is retained at every slow order; the recursion consumes no further strip width.