Explicit positive-order axis matrices

The matrices are obtained by splitting the positive-order convolutions into their two endpoint terms and their strictly lower-order source. No matrix identity or existence of a transformed system is assumed.

structure NavierStokes.PositiveAxisSystem.Jet (K : Type u_1) : Type u_1

Jet data, collecting value, radial, radial2, parameter.

• value : K

  Value of Jet, of type K.

• radial : K

  Radial of Jet, of type K.

• radial2 : K

  Radial2 of Jet, of type K.

• parameter : K

  Parameter of Jet, of type K.

structure NavierStokes.PositiveAxisSystem.BaseJet (K : Type u_1) : Type u_1

Base jet data, collecting phi, axial, beta.

• phi : Jet K

  Phi of BaseJet, of type Jet K.

• axial : Jet K

  Axial of BaseJet, of type Jet K.

• beta : K

  Beta of BaseJet, of type K.

structure NavierStokes.PositiveAxisSystem.SourceJet (K : Type u_1) : Type u_1

The first two entries are the lower-order convective sums minus the known preceding axial diffusion. The last two give the lower pressure convolution and the smooth quotient Ω_(n-1)/X.

• angular : K

  Angular of SourceJet, of type K.

• axial : K

  Axial of SourceJet, of type K.

• pressureProduct : K

  Pressure product of SourceJet, of type K.

• omegaQuotient : K

  Omega quotient of SourceJet, of type K.

noncomputable def NavierStokes.PositiveAxisSystem.a {K : Type u_1} [Field K] (h : K) : K

A, given by 1 / 2 + h.

Equations

• NavierStokes.PositiveAxisSystem.a h = 1 / 2 + h

noncomputable def NavierStokes.PositiveAxisSystem.dScale {K : Type u_1} [Field K] (h : K) : K

D scale, given by 1 / 2 - h.

Equations

• NavierStokes.PositiveAxisSystem.dScale h = 1 / 2 - h

noncomputable def NavierStokes.PositiveAxisSystem.edge {K : Type u_1} [Field K] (eta : K) : K

Edge, given by 1 - eta ^ 2.

Equations

• NavierStokes.PositiveAxisSystem.edge eta = 1 - eta ^ 2

noncomputable def NavierStokes.PositiveAxisSystem.ell {K : Type u_1} [Field K] (h eta : K) : K

Ell, given by 1 - 2 * h * eta ^ 2.

Equations

• NavierStokes.PositiveAxisSystem.ell h eta = 1 - 2 * h * eta ^ 2

noncomputable def NavierStokes.PositiveAxisSystem.angularPower {K : Type u_1} [Field K] (h : K) : K

Angular power, given by -a h - 1 / 2.

Equations

• NavierStokes.PositiveAxisSystem.angularPower h = -NavierStokes.PositiveAxisSystem.a h - 1 / 2

noncomputable def NavierStokes.PositiveAxisSystem.axialPower {K : Type u_1} [Field K] (h : K) : K

Axial power, given by -a h.

Equations

• NavierStokes.PositiveAxisSystem.axialPower h = -NavierStokes.PositiveAxisSystem.a h

noncomputable def NavierStokes.PositiveAxisSystem.inverseSquare {K : Type u_1} [Field K] (C : K) : K

Inverse square, given by (C ^ 2)⁻¹.

Equations

• NavierStokes.PositiveAxisSystem.inverseSquare C = (C ^ 2)⁻¹

noncomputable def NavierStokes.PositiveAxisSystem.timeValue {K : Type u_1} [Field K] (h power eta X : K) (j : Jet K) : K

Time value, given by (-power * j.value + dScale h * eta * j.parameter + X * j.radial) / ell h eta.

Equations

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

noncomputable def NavierStokes.PositiveAxisSystem.axialValue {K : Type u_1} [Field K] (h power eta X : K) (j : Jet K) : K

Axial value, given by (2 * eta * power * j.value + edge eta * j.parameter - 2 * eta * X * j.radial) / ell h eta.

Equations

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

noncomputable def NavierStokes.PositiveAxisSystem.betaValue {K : Type u_1} [Field K] (h lam eta : K) (u k : Jet K) : K

The quotient V_n/X obtained from (21) with Ubar_n=U_n+K_n.

Equations

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

noncomputable def NavierStokes.PositiveAxisSystem.pressureSource {K : Type u_1} [Field K] (C : K) (s : SourceJet K) : K

Pressure source, given by inverseSquare C * s.pressureProduct - s.omegaQuotient / 2.

Equations

• NavierStokes.PositiveAxisSystem.pressureSource C s = NavierStokes.PositiveAxisSystem.inverseSquare C * s.pressureProduct - s.omegaQuotient / 2

noncomputable def NavierStokes.PositiveAxisSystem.pressureValue {K : Type u_1} [Field K] (C : K) (b : BaseJet K) (s : SourceJet K) (phi : Jet K) : K

Pressure value, given by 2 * inverseSquare C * b.phi.value * phi.value + pressureSource C s.

Equations

• NavierStokes.PositiveAxisSystem.pressureValue C b s phi = 2 * NavierStokes.PositiveAxisSystem.inverseSquare C * b.phi.value * phi.value + NavierStokes.PositiveAxisSystem.pressureSource C s

noncomputable def NavierStokes.PositiveAxisSystem.angularRHS {K : Type u_1} [Field K] (h lam eta X : K) (b : BaseJet K) (s : SourceJet K) (phi u k : Jet K) : K

Angular RHS, constructed using timeValue.

Equations

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

noncomputable def NavierStokes.PositiveAxisSystem.axialRHS {K : Type u_1} [Field K] (h lam eta X : K) (b : BaseJet K) (s : SourceJet K) (_phi u k p : Jet K) : K

Axial RHS, constructed using timeValue.

Equations

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

def NavierStokes.PositiveAxisSystem.ExpandedEquations {K : Type u_1} [Field K] (h lam C eta X : K) (b : BaseJet K) (s : SourceJet K) (phi u k p : Jet K) : Prop

The four equations remaining after the first two components of W have been defined as radial derivatives. These are the expanded (21)--(22).

Equations

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

noncomputable def NavierStokes.PositiveAxisSystem.diagonal {K : Type u_1} [Field K] : Fin 6 → K

Diagonal, given by ![0, 0, 2, 0, 3, 1].

Equations

• NavierStokes.PositiveAxisSystem.diagonal = ![0, 0, 2, 0, 3, 1]

noncomputable def NavierStokes.PositiveAxisSystem.jetVector {K : Type u_1} [Field K] (r : K) (phi u k p : Jet K) : Fin 6 → K

Jet vector, given by ![phi.value, u.value, k.value, p.value, 2 * r * phi.radial, 2 * r * u.radial].

Equations

• NavierStokes.PositiveAxisSystem.jetVector r phi u k p = ![phi.value, u.value, k.value, p.value, 2 * r * phi.radial, 2 * r * u.radial]

noncomputable def NavierStokes.PositiveAxisSystem.radialJetVector {K : Type u_1} [Field K] (r : K) (phi u k p : Jet K) : Fin 6 → K

Radial jet vector as an element of Fin 6 → K.

Equations

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

noncomputable def NavierStokes.PositiveAxisSystem.parameterJetVector {K : Type u_1} (phi u k p : Jet K) (q₄ q₅ : K) : Fin 6 → K

Only the first four parameter derivatives enter the system.

Equations

• NavierStokes.PositiveAxisSystem.parameterJetVector phi u k p q₄ q₅ = ![phi.parameter, u.parameter, k.parameter, p.parameter, q₄, q₅]

noncomputable def NavierStokes.PositiveAxisSystem.A0 {K : Type u_1} [Field K] (h lam C r eta : K) (b : BaseJet K) : Matrix (Fin 6) (Fin 6) K

A0 as an element of Matrix (Fin 6) (Fin 6) K.

Equations

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

noncomputable def NavierStokes.PositiveAxisSystem.A1 {K : Type u_1} [Field K] (h r eta : K) (b : BaseJet K) : Matrix (Fin 6) (Fin 6) K

A1 as an element of Matrix (Fin 6) (Fin 6) K.

Equations

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

noncomputable def NavierStokes.PositiveAxisSystem.forcing {K : Type u_1} [Field K] (h C r eta : K) (s : SourceJet K) : Fin 6 → K

Forcing, given by ![0, 0, 0, 2 * r * pressureSource C s, 2 * s.angular, 2 * s.axial - 4 * eta * r ^ 2 * pressureSource C s / ell h eta].

Equations

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

noncomputable def NavierStokes.PositiveAxisSystem.matrixRHS {K : Type u_1} [Field K] (h lam C r eta : K) (b : BaseJet K) (s : SourceJet K) (w v : Fin 6 → K) : Fin 6 → K

Matrix RHS, given by (A0 h lam C r eta b).mulVec w + (A1 h r eta b).mulVec v + forcing h C r eta s.

Equations

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

def NavierStokes.PositiveAxisSystem.JetSystem {K : Type u_1} [Field K] (h lam C r eta : K) (b : BaseJet K) (s : SourceJet K) (phi u k p : Jet K) (q₄ q₅ : K) : Prop

Jet system as an element of Prop.

Equations

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

theorem NavierStokes.PositiveAxisSystem.A1_shape {K : Type u_1} [Field K] (h r eta : K) (b : BaseJet K) (i j : Fin 6) (hij : ↑i < 4 ∨ 4 ≤ ↑j) : A1 h r eta b i j = 0

theorem NavierStokes.PositiveAxisSystem.A1_high_parameters_irrelevant {K : Type u_1} [Field K] (h r eta : K) (b : BaseJet K) (phi u k p : Jet K) (q₄ q₅ q₄' q₅' : K) : (A1 h r eta b).mulVec (parameterJetVector phi u k p q₄ q₅) = (A1 h r eta b).mulVec (parameterJetVector phi u k p q₄' q₅')

theorem NavierStokes.PositiveAxisSystem.matrixRHS_jet {K : Type u_1} [Field K] [CharZero K] (h lam C r eta : K) (b : BaseJet K) (s : SourceJet K) (phi u k p : Jet K) (q₄ q₅ : K) : matrixRHS h lam C r eta b s (jetVector r phi u k p) (parameterJetVector phi u k p q₄ q₅) = ![2 * r * phi.radial, 2 * r * u.radial, -2 * r * u.radial, 2 * r * pressureValue C b s phi, 2 * angularRHS h lam eta (r ^ 2) b s phi u k, 2 * axialRHS h lam eta (r ^ 2) b s phi u k { value := p.value, radial := pressureValue C b s phi, radial2 := p.radial2, parameter := p.parameter }]

Direct multiplication of the displayed matrices reproduces the expanded right sides, with the pressure radial derivative explicitly substituted.

theorem NavierStokes.PositiveAxisSystem.jetSystem_iff_expanded {K : Type u_1} [Field K] [CharZero K] {h lam C r eta : K} (hr : r ≠ 0) (b : BaseJet K) (s : SourceJet K) (phi u k p : Jet K) (q₄ q₅ : K) : JetSystem h lam C r eta b s phi u k p q₄ q₅ ↔ ExpandedEquations h lam C eta (r ^ 2) b s phi u k p

Equivalence with the expanded profile equations, including the average row and the pressure-row substitution. Only the change of radial coordinate requires r≠0; the matrices themselves are nonsingular at the axis.

noncomputable def NavierStokes.PositiveAxisSystem.slowPower {K : Type u_1} [Field K] (h : K) (n : ℕ) : K

Slow exponent at order n.

Equations

• NavierStokes.PositiveAxisSystem.slowPower h n = 2 * ↑n * h

noncomputable def NavierStokes.PositiveAxisSystem.convolution {K : Type u_1} [Field K] (n : ℕ) (F : ℕ → ℕ → K) : K

The coefficient of a Cauchy product at the indicated order.

Equations

• NavierStokes.PositiveAxisSystem.convolution n F = ∑ i ∈ Finset.range (n + 1), F i (n - i)

noncomputable def NavierStokes.PositiveAxisSystem.lowerConvolution {K : Type u_1} [Field K] (n : ℕ) (F : ℕ → ℕ → K) : K

Both indices in this sum are strictly below a positive order n.

Equations

• NavierStokes.PositiveAxisSystem.lowerConvolution n F = ∑ i ∈ Finset.range (n - 1), F (i + 1) (n - (i + 1))

theorem NavierStokes.PositiveAxisSystem.convolution_split {K : Type u_1} [Field K] {n : ℕ} (hn : 0 < n) (F : ℕ → ℕ → K) : convolution n F = F 0 n + F n 0 + lowerConvolution n F

theorem NavierStokes.PositiveAxisSystem.lower_indices {n i : ℕ} (hi : i ∈ Finset.range (n - 1)) : 0 < i + 1 ∧ i + 1 < n ∧ 0 < n - (i + 1) ∧ n - (i + 1) < n

theorem NavierStokes.PositiveAxisSystem.lowerConvolution_congr {K : Type u_1} [Field K] {n : ℕ} {F G : ℕ → ℕ → K} (h : ∀ i < n, ∀ j < n, F i j = G i j) : lowerConvolution n F = lowerConvolution n G

noncomputable def NavierStokes.PositiveAxisSystem.angularConvection {K : Type u_1} [Field K] (h eta X : K) (phi u : ℕ → Jet K) (beta : ℕ → K) (i j : ℕ) : K

Angular convection, given by beta i * (X * (phi j).radial + (phi j).value) + (u i).value * axialValue h (angularPower h + slowPower h j) eta X (phi j).

Equations

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

noncomputable def NavierStokes.PositiveAxisSystem.axialConvection {K : Type u_1} [Field K] (h eta X : K) (u : ℕ → Jet K) (beta : ℕ → K) (i j : ℕ) : K

Axial convection, given by beta i * X * (u j).radial + (u i).value * axialValue h (axialPower h + slowPower h j) eta X (u j).

Equations

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

noncomputable def NavierStokes.PositiveAxisSystem.lowerSource {K : Type u_1} [Field K] (h eta X : K) (n : ℕ) (phi u : ℕ → Jet K) (beta : ℕ → K) (previousAngularDiffusion previousAxialDiffusion omegaQuotient : K) : SourceJet K

The known functions supplied here are exactly the previous-order axial viscosities and the smooth extension of the previous radial residual divided by X; no current-order unknown occurs in this source.

Equations

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

noncomputable def NavierStokes.PositiveAxisSystem.baseAtOrderZero {K : Type u_1} (phi u : ℕ → Jet K) (beta : ℕ → K) : BaseJet K

Base at order zero, given by ⟨phi 0, u 0, beta 0⟩.

Equations

• NavierStokes.PositiveAxisSystem.baseAtOrderZero phi u beta = { phi := phi 0, axial := u 0, beta := beta 0 }

theorem NavierStokes.PositiveAxisSystem.betaValue_eq_average_formula {K : Type u_1} [Field K] [CharZero K] (h lam eta : K) (u k : Jet K) : betaValue h lam eta u k = (2 * eta * u.value - 2 * eta * (dScale h + lam) * (u.value + k.value) - edge eta * (u.parameter + k.parameter)) / ell h eta

The beta formula is precisely (21), with Ubar=U+K.

theorem NavierStokes.PositiveAxisSystem.angularConvection_radial_term {K : Type u_1} [Field K] {X : K} (hX : X ≠ 0) (beta f fx : K) : beta * (X * fx + f) = X * beta * (fx + f / X)

Replacing V=X beta in the angular convection is exact away from the axis.

theorem NavierStokes.PositiveAxisSystem.angularRHS_eq_convolution {K : Type u_1} [Field K] (h eta X : K) {n : ℕ} (hn : 0 < n) (phi u : ℕ → Jet K) (beta : ℕ → K) (k : Jet K) (previousAngularDiffusion previousAxialDiffusion omegaQuotient : K) (hbeta : beta n = betaValue h (slowPower h n) eta (u n) k) : angularRHS h (slowPower h n) eta X (baseAtOrderZero phi u beta) (lowerSource h eta X n phi u beta previousAngularDiffusion previousAxialDiffusion omegaQuotient) (phi n) (u n) k = timeValue h (angularPower h + slowPower h n) eta X (phi n) + convolution n (angularConvection h eta X phi u beta) - previousAngularDiffusion

Endpoint extraction, including the exact lower-order sums.

theorem NavierStokes.PositiveAxisSystem.axialRHS_eq_convolution {K : Type u_1} [Field K] (h eta X : K) {n : ℕ} (hn : 0 < n) (phi u : ℕ → Jet K) (beta : ℕ → K) (k p : Jet K) (previousAngularDiffusion previousAxialDiffusion omegaQuotient : K) (hbeta : beta n = betaValue h (slowPower h n) eta (u n) k) : axialRHS h (slowPower h n) eta X (baseAtOrderZero phi u beta) (lowerSource h eta X n phi u beta previousAngularDiffusion previousAxialDiffusion omegaQuotient) (phi n) (u n) k p = timeValue h (axialPower h + slowPower h n) eta X (u n) + convolution n (axialConvection h eta X u beta) + axialValue h (-2 * a h + slowPower h n) eta X p - previousAxialDiffusion

theorem NavierStokes.PositiveAxisSystem.pressureValue_eq_convolution {K : Type u_1} [Field K] [CharZero K] (h C eta X : K) {n : ℕ} (hn : 0 < n) (phi u : ℕ → Jet K) (beta : ℕ → K) (previousAngularDiffusion previousAxialDiffusion omegaQuotient : K) : pressureValue C (baseAtOrderZero phi u beta) (lowerSource h eta X n phi u beta previousAngularDiffusion previousAxialDiffusion omegaQuotient) (phi n) = (inverseSquare C * convolution n fun (i j : ℕ) => (phi i).value * (phi j).value) - omegaQuotient / 2

def NavierStokes.PositiveAxisSystem.PositiveOrderEquations {K : Type u_1} [Field K] (h C eta X : K) (n : ℕ) (phi u : ℕ → Jet K) (beta : ℕ → K) (k p : Jet K) (previousAngularDiffusion previousAxialDiffusion omegaQuotient : K) : Prop

Positive-order equations (22) before extraction of the endpoint terms. The average relation is the derivative of X Ubar = ∫₀ˣ U, with K=Ubar-U. The beta hypothesis in the equivalence below is the second identity of (21).

Equations

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

theorem NavierStokes.PositiveAxisSystem.expanded_iff_positiveOrder {K : Type u_1} [Field K] [CharZero K] (h C eta X : K) {n : ℕ} (hn : 0 < n) (phi u : ℕ → Jet K) (beta : ℕ → K) (k p : Jet K) (previousAngularDiffusion previousAxialDiffusion omegaQuotient : K) (hbeta : beta n = betaValue h (slowPower h n) eta (u n) k) : ExpandedEquations h (slowPower h n) C eta X (baseAtOrderZero phi u beta) (lowerSource h eta X n phi u beta previousAngularDiffusion previousAxialDiffusion omegaQuotient) (phi n) (u n) k p ↔ PositiveOrderEquations h C eta X n phi u beta k p previousAngularDiffusion previousAxialDiffusion omegaQuotient

theorem NavierStokes.PositiveAxisSystem.jetSystem_iff_positiveOrder {K : Type u_1} [Field K] [CharZero K] (h C r eta : K) (hr : r ≠ 0) {n : ℕ} (hn : 0 < n) (phi u : ℕ → Jet K) (beta : ℕ → K) (k p : Jet K) (q₄ q₅ previousAngularDiffusion previousAxialDiffusion omegaQuotient : K) (hbeta : beta n = betaValue h (slowPower h n) eta (u n) k) : JetSystem h (slowPower h n) C r eta (baseAtOrderZero phi u beta) (lowerSource h eta (r ^ 2) n phi u beta previousAngularDiffusion previousAxialDiffusion omegaQuotient) (phi n) (u n) k p q₄ q₅ ↔ PositiveOrderEquations h C eta (r ^ 2) n phi u beta k p previousAngularDiffusion previousAxialDiffusion omegaQuotient

noncomputable def NavierStokes.PositiveAxisSystem.actualJet (f : SimilarityProfile.InnerProfile) (w : SimilarityProfile.InnerPoint) : Jet ℝ

Jets here are actual Fréchet partial derivatives of real profiles.

Equations

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

theorem NavierStokes.PositiveAxisSystem.timeValue_actualJet (h b : ℝ) (f : SimilarityProfile.InnerProfile) (w : SimilarityProfile.InnerPoint) : timeValue h b w.2 w.1 (actualJet f w) = SimilarityProfile.T h b f w

theorem NavierStokes.PositiveAxisSystem.axialValue_actualJet (h b : ℝ) (f : SimilarityProfile.InnerProfile) (w : SimilarityProfile.InnerPoint) : axialValue h b w.2 w.1 (actualJet f w) = SimilarityProfile.Z h b f w

theorem NavierStokes.PositiveAxisSystem.partialX_contDiffAt {f : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hf : ContDiffAt ℝ 2 f w) : ContDiffAt ℝ 1 (SimilarityProfile.partialX f) w

theorem NavierStokes.PositiveAxisSystem.hasDerivAt_squareProfile {f : SimilarityProfile.InnerProfile} {r eta : ℝ} (hf : DifferentiableAt ℝ f (r ^ 2, eta)) : HasDerivAt (fun (s : ℝ) => f (s ^ 2, eta)) (2 * r * SimilarityProfile.partialX f (r ^ 2, eta)) r

theorem NavierStokes.PositiveAxisSystem.hasDerivAt_parameterProfile {f : SimilarityProfile.InnerProfile} {X eta : ℝ} (hf : DifferentiableAt ℝ f (X, eta)) : HasDerivAt (fun (z : ℝ) => f (X, z)) (SimilarityProfile.partialEta f (X, eta)) eta

theorem NavierStokes.PositiveAxisSystem.hasDerivAt_squareProfile_radial {f : SimilarityProfile.InnerProfile} {r eta : ℝ} (hf : ContDiffAt ℝ 2 f (r ^ 2, eta)) : HasDerivAt (fun (s : ℝ) => 2 * s * SimilarityProfile.partialX f (s ^ 2, eta)) (2 * SimilarityProfile.partialX f (r ^ 2, eta) + 4 * r ^ 2 * SimilarityProfile.partialX (SimilarityProfile.partialX f) (r ^ 2, eta)) r

noncomputable def NavierStokes.PositiveAxisSystem.profileVector (phi u k p : SimilarityProfile.InnerProfile) (r eta : ℝ) : Fin 6 → ℝ

Profile vector, given by jetVector r (actualJet phi (r ^ 2, eta)) (actualJet u (r ^ 2, eta)) (actualJet k (r ^ 2, eta)) (actualJet p (r ^ 2, eta)).

Equations

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

theorem NavierStokes.PositiveAxisSystem.profileVector_radial {phi u k p : SimilarityProfile.InnerProfile} {r eta : ℝ} (hphi : ContDiffAt ℝ 2 phi (r ^ 2, eta)) (hu : ContDiffAt ℝ 2 u (r ^ 2, eta)) (hk : DifferentiableAt ℝ k (r ^ 2, eta)) (hp : DifferentiableAt ℝ p (r ^ 2, eta)) : (fun (i : Fin 6) => deriv (fun (s : ℝ) => profileVector phi u k p s eta i) r) = radialJetVector r (actualJet phi (r ^ 2, eta)) (actualJet u (r ^ 2, eta)) (actualJet k (r ^ 2, eta)) (actualJet p (r ^ 2, eta))

theorem NavierStokes.PositiveAxisSystem.profileVector_parameter {phi u k p : SimilarityProfile.InnerProfile} {r eta : ℝ} (hphi : DifferentiableAt ℝ phi (r ^ 2, eta)) (hu : DifferentiableAt ℝ u (r ^ 2, eta)) (hk : DifferentiableAt ℝ k (r ^ 2, eta)) (hp : DifferentiableAt ℝ p (r ^ 2, eta)) : (fun (i : Fin 6) => deriv (fun (z : ℝ) => profileVector phi u k p r z i) eta) = parameterJetVector (actualJet phi (r ^ 2, eta)) (actualJet u (r ^ 2, eta)) (actualJet k (r ^ 2, eta)) (actualJet p (r ^ 2, eta)) (deriv (fun (z : ℝ) => profileVector phi u k p r z 4) eta) (deriv (fun (z : ℝ) => profileVector phi u k p r z 5) eta)

def NavierStokes.PositiveAxisSystem.ProfileSystem (h lam C r eta : ℝ) (b : BaseJet ℝ) (s : SourceJet ℝ) (phi u k p : SimilarityProfile.InnerProfile) : Prop

The displayed first-order system uses actual derivatives of the actual profiles, not independent formal jet variables.

Equations

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

theorem NavierStokes.PositiveAxisSystem.profileSystem_iff_expanded {h lam C r eta : ℝ} (hr : r ≠ 0) (b : BaseJet ℝ) (s : SourceJet ℝ) {phi u k p : SimilarityProfile.InnerProfile} (hphi : ContDiffAt ℝ 2 phi (r ^ 2, eta)) (hu : ContDiffAt ℝ 2 u (r ^ 2, eta)) (hk : DifferentiableAt ℝ k (r ^ 2, eta)) (hp : DifferentiableAt ℝ p (r ^ 2, eta)) : ProfileSystem h lam C r eta b s phi u k p ↔ ExpandedEquations h lam C eta (r ^ 2) b s (actualJet phi (r ^ 2, eta)) (actualJet u (r ^ 2, eta)) (actualJet k (r ^ 2, eta)) (actualJet p (r ^ 2, eta))

noncomputable def NavierStokes.PositiveAxisSystem.precedingDiffusion (h power : ℝ) (F : ℕ → SimilarityProfile.InnerProfile) (n : ℕ) : SimilarityProfile.InnerProfile

The preceding axial viscosity uses the actual similarity operator twice. The negative-order term at order zero is zero.

Equations

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

theorem NavierStokes.PositiveAxisSystem.precedingDiffusion_congr (h power : ℝ) {F G : ℕ → SimilarityProfile.InnerProfile} {n : ℕ} (hFG : ∀ j < n, F j = G j) : precedingDiffusion h power F n = precedingDiffusion h power G n

noncomputable def NavierStokes.PositiveAxisSystem.actualLowerSource (h : ℝ) (n : ℕ) (phi u beta : ℕ → SimilarityProfile.InnerProfile) (omegaQuotient : SimilarityProfile.InnerProfile) (w : SimilarityProfile.InnerPoint) : SourceJet ℝ

Fully specified source from lower-order profile jets and a supplied regular representative of the preceding Ω/X.

Equations

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

theorem NavierStokes.PositiveAxisSystem.actualLowerSource_congr (h : ℝ) {n : ℕ} {phi u beta phi' u' beta' : ℕ → SimilarityProfile.InnerProfile} (omegaQuotient : SimilarityProfile.InnerProfile) (hphi : ∀ j < n, phi j = phi' j) (hu : ∀ j < n, u j = u' j) (hbeta : ∀ j < n, beta j = beta' j) (w : SimilarityProfile.InnerPoint) : actualLowerSource h n phi u beta omegaQuotient w = actualLowerSource h n phi' u' beta' omegaQuotient w

theorem NavierStokes.PositiveAxisSystem.actualLowerSource_update (h : ℝ) (n : ℕ) (phi u beta : ℕ → SimilarityProfile.InnerProfile) (phiNew uNew betaNew omegaQuotient : SimilarityProfile.InnerProfile) (w : SimilarityProfile.InnerPoint) : actualLowerSource h n (Function.update phi n phiNew) (Function.update u n uNew) (Function.update beta n betaNew) omegaQuotient w = actualLowerSource h n phi u beta omegaQuotient w

theorem NavierStokes.PositiveAxisSystem.baseAtOrderZero_update {n : ℕ} (hn : 0 < n) (phi u beta : ℕ → SimilarityProfile.InnerProfile) (phiNew uNew betaNew : SimilarityProfile.InnerProfile) (w : SimilarityProfile.InnerPoint) : (baseAtOrderZero (fun (j : ℕ) => actualJet (Function.update phi n phiNew j) w) (fun (j : ℕ) => actualJet (Function.update u n uNew j) w) fun (j : ℕ) => Function.update beta n betaNew j w) = baseAtOrderZero (fun (j : ℕ) => actualJet (phi j) w) (fun (j : ℕ) => actualJet (u j) w) fun (j : ℕ) => beta j w

theorem NavierStokes.PositiveAxisSystem.profileSystem_iff_positiveOrder {h C r eta : ℝ} (hr : r ≠ 0) {n : ℕ} (hn : 0 < n) (phi u beta : ℕ → SimilarityProfile.InnerProfile) (k p omegaQuotient : SimilarityProfile.InnerProfile) (hphi : ContDiffAt ℝ 2 (phi n) (r ^ 2, eta)) (hu : ContDiffAt ℝ 2 (u n) (r ^ 2, eta)) (hk : DifferentiableAt ℝ k (r ^ 2, eta)) (hp : DifferentiableAt ℝ p (r ^ 2, eta)) (hbeta : beta n (r ^ 2, eta) = betaValue h (slowPower h n) eta (actualJet (u n) (r ^ 2, eta)) (actualJet k (r ^ 2, eta))) : ProfileSystem h (slowPower h n) C r eta (baseAtOrderZero (fun (j : ℕ) => actualJet (phi j) (r ^ 2, eta)) (fun (j : ℕ) => actualJet (u j) (r ^ 2, eta)) fun (j : ℕ) => beta j (r ^ 2, eta)) (actualLowerSource h n phi u beta omegaQuotient (r ^ 2, eta)) (phi n) (u n) k p ↔ PositiveOrderEquations h C eta (r ^ 2) n (fun (j : ℕ) => actualJet (phi j) (r ^ 2, eta)) (fun (j : ℕ) => actualJet (u j) (r ^ 2, eta)) (fun (j : ℕ) => beta j (r ^ 2, eta)) (actualJet k (r ^ 2, eta)) (actualJet p (r ^ 2, eta)) (precedingDiffusion h (angularPower h) phi n (r ^ 2, eta)) (precedingDiffusion h (axialPower h) u n (r ^ 2, eta)) (omegaQuotient (r ^ 2, eta))

End-to-end equivalence from the actual profile derivatives to the positive-order convolution equations, with all finite source terms displayed.

noncomputable def NavierStokes.PositiveAxisSystem.averageDefect (u : SimilarityProfile.InnerProfile) : SimilarityProfile.InnerProfile

The actual radial-average difference, with its regular value at the axis.

Equations

• NavierStokes.PositiveAxisSystem.averageDefect u w = NavierStokes.ProfileHistories.average u w - u w

theorem NavierStokes.PositiveAxisSystem.averageDefect_smooth (Ω : ProfileHistories.RadialDomain) {u : SimilarityProfile.InnerProfile} (hu : ContDiffOn ℝ (↑⊤) u Ω.carrier) : ContDiffOn ℝ (↑⊤) (averageDefect u) Ω.carrier

theorem NavierStokes.PositiveAxisSystem.averageDefect_radial (Ω : ProfileHistories.RadialDomain) {u : SimilarityProfile.InnerProfile} (hu : ContDiffOn ℝ (↑⊤) u Ω.carrier) {w : SimilarityProfile.InnerPoint} (hw : w ∈ Ω.carrier) : w.1 * (SimilarityProfile.partialX u w + SimilarityProfile.partialX (averageDefect u) w) + averageDefect u w = 0

theorem NavierStokes.PositiveAxisSystem.betaValue_averageDefect (Ω : ProfileHistories.RadialDomain) {u : SimilarityProfile.InnerProfile} (hu : ContDiffOn ℝ (↑⊤) u Ω.carrier) (h lam : ℝ) {w : SimilarityProfile.InnerPoint} (hw : w ∈ Ω.carrier) (hX : w.1 ≠ 0) : betaValue h lam w.2 (actualJet u w) (actualJet (averageDefect u) w) = SlowDivergence.radialFlux h lam u w / w.1

theorem NavierStokes.PositiveAxisSystem.averageDefect_divergence (Ω : ProfileHistories.RadialDomain) {u : SimilarityProfile.InnerProfile} (hu : ContDiffOn ℝ (↑⊤) u Ω.carrier) (h lam : ℝ) {w : SimilarityProfile.InnerPoint} (hw : w ∈ Ω.carrier) (hL : ell h w.2 ≠ 0) : SimilarityProfile.partialX (SlowDivergence.radialFlux h lam u) w = -axialValue h (-a h + lam) w.2 w.1 (actualJet u w)

Both identities in (21) hold for the same actual reconstructed flux.

theorem NavierStokes.PositiveAxisSystem.averageDefect_unique (Ω : ProfileHistories.RadialDomain) {u k : SimilarityProfile.InnerProfile} (hu : ContDiffOn ℝ (↑⊤) u Ω.carrier) (hk : ContDiffOn ℝ (↑⊤) k Ω.carrier) (hrow : ∀ w ∈ Ω.carrier, w.1 * (SimilarityProfile.partialX u w + SimilarityProfile.partialX k w) + k w = 0) {w : SimilarityProfile.InnerPoint} (hw : w ∈ Ω.carrier) : k w = averageDefect u w

The regular average row also recovers the actual radial average. Thus a smooth solution's third component cannot be an independent auxiliary field.

@[reducible, inline]

abbrev NavierStokes.PositiveAxisSystem.CoefficientData : Type

The eleven finite input jets are, in order: φ₀, ∂Xφ₀, ∂ηφ₀, U₀, ∂XU₀, ∂ηU₀, β₀, followed by the angular source, axial source, lower pressure product, and regular quotient Ω_(n-1)/X. Regularity is required of these actual finite jets, not inferred from separate smoothness of a lower-order profile.

Equations

• NavierStokes.PositiveAxisSystem.CoefficientData = (Fin 11 → ℝ × ℂ → ℂ)

noncomputable def NavierStokes.PositiveAxisSystem.coefficientBase (F : CoefficientData) (X : ℝ) (z : ℂ) : BaseJet ℂ

Coefficient base, given by ⟨⟨F 0 (X, z), F 1 (X, z), 0, F 2 (X, z)⟩, ⟨F 3 (X, z), F 4 (X, z), 0, F 5 (X, z)⟩, F 6 (X, z)⟩.

Equations

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

noncomputable def NavierStokes.PositiveAxisSystem.coefficientSource (F : CoefficientData) (X : ℝ) (z : ℂ) : SourceJet ℂ

Coefficient source, given by ⟨F 7 (X, z), F 8 (X, z), F 9 (X, z), F 10 (X, z)⟩.

Equations

• NavierStokes.PositiveAxisSystem.coefficientSource F X z = { angular := F 7 (X, z), axial := F 8 (X, z), pressureProduct := F 9 (X, z), omegaQuotient := F 10 (X, z) }

noncomputable def NavierStokes.PositiveAxisSystem.coefficient0 (h lam C : ℂ) (F : CoefficientData) : VolterraAnalyticBounds.Coeff

Coefficient0, defined pointwise by A0 h lam C (r : ℂ) z (coefficientBase F (r ^ 2) z).

Equations

• NavierStokes.PositiveAxisSystem.coefficient0 h lam C F r z = NavierStokes.PositiveAxisSystem.A0 h lam C (↑r) z (NavierStokes.PositiveAxisSystem.coefficientBase F (r ^ 2) z)

noncomputable def NavierStokes.PositiveAxisSystem.coefficient1 (h : ℂ) (F : CoefficientData) : VolterraAnalyticBounds.Coeff

Coefficient1, defined pointwise by A1 h (r : ℂ) z (coefficientBase F (r ^ 2) z).

Equations

• NavierStokes.PositiveAxisSystem.coefficient1 h F r z = NavierStokes.PositiveAxisSystem.A1 h (↑r) z (NavierStokes.PositiveAxisSystem.coefficientBase F (r ^ 2) z)

noncomputable def NavierStokes.PositiveAxisSystem.sourceField (h C : ℂ) (F : CoefficientData) : VolterraAnalyticBounds.Field

Source field, defined pointwise by forcing h C (r : ℂ) z (coefficientSource F (r ^ 2) z).

Equations

• NavierStokes.PositiveAxisSystem.sourceField h C F r z = NavierStokes.PositiveAxisSystem.forcing h C (↑r) z (NavierStokes.PositiveAxisSystem.coefficientSource F (r ^ 2) z)

theorem NavierStokes.PositiveAxisSystem.coefficient1_shape (h : ℂ) (F : CoefficientData) : VolterraAnalyticBounds.DerivativeShape (coefficient1 h F)

theorem NavierStokes.PositiveAxisSystem.diagonal_eq_exponent (i : Fin 6) : diagonal i = ↑(VolterraAnalyticBounds.exponent i)

theorem NavierStokes.PositiveAxisSystem.coefficient0_parity (h lam C : ℂ) (F : CoefficientData) : VolterraParity.CoefficientParity (coefficient0 h lam C F)

theorem NavierStokes.PositiveAxisSystem.coefficient1_parity (h : ℂ) (F : CoefficientData) : VolterraParity.CoefficientParity (coefficient1 h F)

theorem NavierStokes.PositiveAxisSystem.sourceField_parity (h C : ℂ) (F : CoefficientData) : VolterraParity.ForcingParity (sourceField h C F)

theorem NavierStokes.PositiveAxisSystem.inverse_ell_contDiffAt {n : WithTop ℕ∞} {h : ℂ} {w : ℝ × ℂ} (hL : ell h w.2 ≠ 0) : ContDiffAt ℝ n (fun (v : ℝ × ℂ) => (ell h v.2)⁻¹) w

theorem NavierStokes.PositiveAxisSystem.inverse_ell_analyticAt {h z : ℂ} (hL : ell h z ≠ 0) : AnalyticAt ℂ (fun (v : ℂ) => (ell h v)⁻¹) z

theorem NavierStokes.PositiveAxisSystem.coefficient0_contDiffAt_of_pullback {n : WithTop ℕ∞} {h lam C : ℂ} {F : CoefficientData} {w : ℝ × ℂ} (hF : ∀ (i : Fin 11), ContDiffAt ℝ n (fun (v : ℝ × ℂ) => F i (v.1 ^ 2, v.2)) w) (hL : ell h w.2 ≠ 0) (i j : Fin 6) : ContDiffAt ℝ n (fun (v : ℝ × ℂ) => coefficient0 h lam C F v.1 v.2 i j) w

theorem NavierStokes.PositiveAxisSystem.coefficient1_contDiffAt_of_pullback {n : WithTop ℕ∞} {h : ℂ} {F : CoefficientData} {w : ℝ × ℂ} (hF : ∀ (i : Fin 11), ContDiffAt ℝ n (fun (v : ℝ × ℂ) => F i (v.1 ^ 2, v.2)) w) (hL : ell h w.2 ≠ 0) (i j : Fin 6) : ContDiffAt ℝ n (fun (v : ℝ × ℂ) => coefficient1 h F v.1 v.2 i j) w

theorem NavierStokes.PositiveAxisSystem.sourceField_contDiffAt_of_pullback {n : WithTop ℕ∞} {h C : ℂ} {F : CoefficientData} {w : ℝ × ℂ} (hF : ∀ (i : Fin 11), ContDiffAt ℝ n (fun (v : ℝ × ℂ) => F i (v.1 ^ 2, v.2)) w) (hL : ell h w.2 ≠ 0) (i : Fin 6) : ContDiffAt ℝ n (fun (v : ℝ × ℂ) => sourceField h C F v.1 v.2 i) w

theorem NavierStokes.PositiveAxisSystem.coefficient0_analyticAt {h lam C : ℂ} {F : CoefficientData} {r : ℝ} {z : ℂ} (hF : ∀ (i : Fin 11), AnalyticAt ℂ (fun (v : ℂ) => F i (r ^ 2, v)) z) (hL : ell h z ≠ 0) (i j : Fin 6) : AnalyticAt ℂ (fun (v : ℂ) => coefficient0 h lam C F r v i j) z

theorem NavierStokes.PositiveAxisSystem.coefficient1_analyticAt {h : ℂ} {F : CoefficientData} {r : ℝ} {z : ℂ} (hF : ∀ (i : Fin 11), AnalyticAt ℂ (fun (v : ℂ) => F i (r ^ 2, v)) z) (hL : ell h z ≠ 0) (i j : Fin 6) : AnalyticAt ℂ (fun (v : ℂ) => coefficient1 h F r v i j) z

theorem NavierStokes.PositiveAxisSystem.sourceField_analyticAt {h C : ℂ} {F : CoefficientData} {r : ℝ} {z : ℂ} (hF : ∀ (i : Fin 11), AnalyticAt ℂ (fun (v : ℂ) => F i (r ^ 2, v)) z) (hL : ell h z ≠ 0) (i : Fin 6) : AnalyticAt ℂ (fun (v : ℂ) => sourceField h C F r v i) z

theorem NavierStokes.PositiveAxisSystem.square_pullback_contDiffAt {n : WithTop ℕ∞} {f : ℝ × ℂ → ℂ} {w : ℝ × ℂ} (hf : ContDiffWithinAt ℝ n f (Set.Ici 0 ×ˢ Set.univ) (w.1 ^ 2, w.2)) : ContDiffAt ℝ n (fun (v : ℝ × ℂ) => f (v.1 ^ 2, v.2)) w

One-sided smooth X data suffice for a smooth signed square pullback.

theorem NavierStokes.PositiveAxisSystem.coefficient0_contDiffAt {n : WithTop ℕ∞} {h lam C : ℂ} {F : CoefficientData} {w : ℝ × ℂ} (hF : ∀ (i : Fin 11), ContDiffAt ℝ n (F i) (w.1 ^ 2, w.2)) (hL : ell h w.2 ≠ 0) (i j : Fin 6) : ContDiffAt ℝ n (fun (v : ℝ × ℂ) => coefficient0 h lam C F v.1 v.2 i j) w

theorem NavierStokes.PositiveAxisSystem.coefficient1_contDiffAt {n : WithTop ℕ∞} {h : ℂ} {F : CoefficientData} {w : ℝ × ℂ} (hF : ∀ (i : Fin 11), ContDiffAt ℝ n (F i) (w.1 ^ 2, w.2)) (hL : ell h w.2 ≠ 0) (i j : Fin 6) : ContDiffAt ℝ n (fun (v : ℝ × ℂ) => coefficient1 h F v.1 v.2 i j) w

theorem NavierStokes.PositiveAxisSystem.sourceField_contDiffAt {n : WithTop ℕ∞} {h C : ℂ} {F : CoefficientData} {w : ℝ × ℂ} (hF : ∀ (i : Fin 11), ContDiffAt ℝ n (F i) (w.1 ^ 2, w.2)) (hL : ell h w.2 ≠ 0) (i : Fin 6) : ContDiffAt ℝ n (fun (v : ℝ × ℂ) => sourceField h C F v.1 v.2 i) w

theorem NavierStokes.PositiveAxisSystem.coefficient0_contDiffOn_of_pullback {n : WithTop ℕ∞} {h lam C : ℂ} {F : CoefficientData} {S : Set (ℝ × ℂ)} (hF : ∀ w ∈ S, ∀ (i : Fin 11), ContDiffAt ℝ n (fun (v : ℝ × ℂ) => F i (v.1 ^ 2, v.2)) w) (hL : ∀ w ∈ S, ell h w.2 ≠ 0) (i j : Fin 6) : ContDiffOn ℝ n (fun (v : ℝ × ℂ) => coefficient0 h lam C F v.1 v.2 i j) S

theorem NavierStokes.PositiveAxisSystem.coefficient1_contDiffOn_of_pullback {n : WithTop ℕ∞} {h : ℂ} {F : CoefficientData} {S : Set (ℝ × ℂ)} (hF : ∀ w ∈ S, ∀ (i : Fin 11), ContDiffAt ℝ n (fun (v : ℝ × ℂ) => F i (v.1 ^ 2, v.2)) w) (hL : ∀ w ∈ S, ell h w.2 ≠ 0) (i j : Fin 6) : ContDiffOn ℝ n (fun (v : ℝ × ℂ) => coefficient1 h F v.1 v.2 i j) S

theorem NavierStokes.PositiveAxisSystem.sourceField_contDiffOn_of_pullback {n : WithTop ℕ∞} {h C : ℂ} {F : CoefficientData} {S : Set (ℝ × ℂ)} (hF : ∀ w ∈ S, ∀ (i : Fin 11), ContDiffAt ℝ n (fun (v : ℝ × ℂ) => F i (v.1 ^ 2, v.2)) w) (hL : ∀ w ∈ S, ell h w.2 ≠ 0) (i : Fin 6) : ContDiffOn ℝ n (fun (v : ℝ × ℂ) => sourceField h C F v.1 v.2 i) S

theorem NavierStokes.PositiveAxisSystem.coefficient0_contDiffOn {n : WithTop ℕ∞} {h lam C : ℂ} {F : CoefficientData} {S : Set (ℝ × ℂ)} (hF : ∀ w ∈ S, ∀ (i : Fin 11), ContDiffAt ℝ n (F i) (w.1 ^ 2, w.2)) (hL : ∀ w ∈ S, ell h w.2 ≠ 0) (i j : Fin 6) : ContDiffOn ℝ n (fun (v : ℝ × ℂ) => coefficient0 h lam C F v.1 v.2 i j) S

theorem NavierStokes.PositiveAxisSystem.coefficient1_contDiffOn {n : WithTop ℕ∞} {h : ℂ} {F : CoefficientData} {S : Set (ℝ × ℂ)} (hF : ∀ w ∈ S, ∀ (i : Fin 11), ContDiffAt ℝ n (F i) (w.1 ^ 2, w.2)) (hL : ∀ w ∈ S, ell h w.2 ≠ 0) (i j : Fin 6) : ContDiffOn ℝ n (fun (v : ℝ × ℂ) => coefficient1 h F v.1 v.2 i j) S

theorem NavierStokes.PositiveAxisSystem.sourceField_contDiffOn {n : WithTop ℕ∞} {h C : ℂ} {F : CoefficientData} {S : Set (ℝ × ℂ)} (hF : ∀ w ∈ S, ∀ (i : Fin 11), ContDiffAt ℝ n (F i) (w.1 ^ 2, w.2)) (hL : ∀ w ∈ S, ell h w.2 ≠ 0) (i : Fin 6) : ContDiffOn ℝ n (fun (v : ℝ × ℂ) => sourceField h C F v.1 v.2 i) S

noncomputable def NavierStokes.PositiveAxisSystem.complexJet (j : Jet ℝ) : Jet ℂ

Complex jet, given by ⟨j.value, j.radial, j.radial2, j.parameter⟩.

Equations

• NavierStokes.PositiveAxisSystem.complexJet j = { value := ↑j.value, radial := ↑j.radial, radial2 := ↑j.radial2, parameter := ↑j.parameter }

noncomputable def NavierStokes.PositiveAxisSystem.complexBase (b : BaseJet ℝ) : BaseJet ℂ

Complex base, given by ⟨complexJet b.phi, complexJet b.axial, b.beta⟩.

Equations

• NavierStokes.PositiveAxisSystem.complexBase b = { phi := NavierStokes.PositiveAxisSystem.complexJet b.phi, axial := NavierStokes.PositiveAxisSystem.complexJet b.axial, beta := ↑b.beta }

noncomputable def NavierStokes.PositiveAxisSystem.complexSource (s : SourceJet ℝ) : SourceJet ℂ

Complex source, given by ⟨s.angular, s.axial, s.pressureProduct, s.omegaQuotient⟩.

Equations

• NavierStokes.PositiveAxisSystem.complexSource s = { angular := ↑s.angular, axial := ↑s.axial, pressureProduct := ↑s.pressureProduct, omegaQuotient := ↑s.omegaQuotient }

theorem NavierStokes.PositiveAxisSystem.A0_ofReal (h lam C r eta : ℝ) (b : BaseJet ℝ) : A0 (↑h) (↑lam) (↑C) (↑r) (↑eta) (complexBase b) = (A0 h lam C r eta b).map Complex.ofReal

theorem NavierStokes.PositiveAxisSystem.A1_ofReal (h r eta : ℝ) (b : BaseJet ℝ) : A1 (↑h) (↑r) (↑eta) (complexBase b) = (A1 h r eta b).map Complex.ofReal

theorem NavierStokes.PositiveAxisSystem.forcing_ofReal (h C r eta : ℝ) (s : SourceJet ℝ) : forcing (↑h) (↑C) (↑r) (↑eta) (complexSource s) = fun (i : Fin 6) => ↑(forcing h C r eta s i)

theorem NavierStokes.PositiveAxisSystem.diagonal_ofReal (i : Fin 6) : diagonal i = ↑(diagonal i)

theorem NavierStokes.PositiveAxisSystem.matrixRHS_realPart (h lam C r eta : ℝ) (b : BaseJet ℝ) (s : SourceJet ℝ) (w v : VolterraAnalyticBounds.Vec) (i : Fin 6) : (matrixRHS (↑h) (↑lam) (↑C) (↑r) (↑eta) (complexBase b) (complexSource s) w v i).re = matrixRHS h lam C r eta b s (fun (j : Fin 6) => (w j).re) (fun (j : Fin 6) => (v j).re) i

Taking real parts commutes with the explicit system at real input jets.

noncomputable def NavierStokes.PositiveAxisSystem.realTrace (W : VolterraAnalyticBounds.Field) (r eta : ℝ) (i : Fin 6) : ℝ

Real trace, given by (W r (eta : ℂ) i).re.

Equations

• NavierStokes.PositiveAxisSystem.realTrace W r eta i = (W r (↑eta) i).re

theorem NavierStokes.PositiveAxisSystem.realTrace_solves_system (h lam C r eta : ℝ) (b : BaseJet ℝ) (s : SourceJet ℝ) (W : VolterraAnalyticBounds.Field) (hr : ∀ (i : Fin 6), DifferentiableAt ℝ (fun (q : ℝ) => W q (↑eta) i) r) (hz : ∀ (i : Fin 6), DifferentiableAt ℂ (fun (z : ℂ) => W r z i) ↑eta) (hW : ∀ (i : Fin 6), deriv (fun (q : ℝ) => W q (↑eta) i) r + diagonal i / ↑r * W r (↑eta) i = matrixRHS (↑h) (↑lam) (↑C) (↑r) (↑eta) (complexBase b) (complexSource s) (W r ↑eta) (fun (j : Fin 6) => deriv (fun (z : ℂ) => W r z j) ↑eta) i) (i : Fin 6) : deriv (fun (q : ℝ) => realTrace W q eta i) r + diagonal i / r * realTrace W r eta i = matrixRHS h lam C r eta b s (realTrace W r eta) (fun (j : Fin 6) => deriv (fun (z : ℝ) => realTrace W r z j) eta) i

A complex solution with real coefficients yields a real solution by componentwise real part. Both radial and parameter derivatives in the result are actual real derivatives; no reality of the chosen complex solution is assumed.