From the coefficient fixed point to actual natural-axis profiles

This bridge uses ordinary real derivatives of the evaluated functions. The fixed input data must still be supplied as members of the coefficient space; their construction from the outgoing schedule is a separate obligation.

Actual bounded operators on the compatible natural-axis coefficient space

The numerical bounds come from AxisWeightEstimates. This module additionally proves compatibility of the output jets, so its operators act on actual smooth coefficient functions in the complete space, not just unrelated arrays.

@[instance_reducible]

noncomputable def NavierStokes.AxisOperators.instAxisOperators1 (I : AxisCoefficientSpace.Window) (ε : ℝ) : NormedAddCommGroup ↥(AxisCoefficientSpace.AxisSpace I ε)

Cache the standard NormedAddCommGroup (AxisSpace I ε) instance to shorten typeclass synthesis.

Equations

• NavierStokes.AxisOperators.instAxisOperators1 I ε = inferInstance

@[instance_reducible]

noncomputable def NavierStokes.AxisOperators.instAxisOperators2 (I : AxisCoefficientSpace.Window) (ε : ℝ) : NormedSpace ℝ ↥(AxisCoefficientSpace.AxisSpace I ε)

Cache the standard NormedSpace ℝ (AxisSpace I ε) instance to shorten typeclass synthesis.

Equations

• NavierStokes.AxisOperators.instAxisOperators2 I ε = inferInstance

def NavierStokes.AxisOperators.leibnizSum (f g : ℕ → ℝ) (m : ℕ) : ℝ

The finite Leibniz sum for one parameter derivative order.

Equations

• NavierStokes.AxisOperators.leibnizSum f g m = ∑ kl ∈ Finset.antidiagonal m, ↑(m.choose kl.1) * f kl.1 * g kl.2

theorem NavierStokes.AxisOperators.leibniz_boundary (f g : ℕ → ℝ) (m : ℕ) : ∑ kl ∈ Finset.antidiagonal m, ↑(m.choose kl.1) * f kl.1 * g (kl.2 + 1) = f 0 * g (m + 1) + ∑ kl ∈ Finset.antidiagonal m, ↑(m.choose (kl.1 + 1)) * f (kl.1 + 1) * g kl.2

theorem NavierStokes.AxisOperators.leibnizSum_succ (f g : ℕ → ℝ) (m : ℕ) : leibnizSum f g (m + 1) = leibnizSum (fun (k : ℕ) => f (k + 1)) g m + leibnizSum f (fun (l : ℕ) => g (l + 1)) m

Pascal's identity is exactly the derivative recurrence for the Leibniz sum.

theorem NavierStokes.AxisOperators.continuousOn_leibnizSum (I : AxisCoefficientSpace.Window) (f g : ℕ → ℝ → ℝ) (hf : ∀ (k : ℕ), ContinuousOn (f k) I.interval) (hg : ∀ (k : ℕ), ContinuousOn (g k) I.interval) (m : ℕ) : ContinuousOn (fun (x : ℝ) => leibnizSum (fun (k : ℕ) => f k x) (fun (k : ℕ) => g k x) m) I.interval

theorem NavierStokes.AxisOperators.hasDerivWithinAt_leibnizSum (I : AxisCoefficientSpace.Window) (f g : ℕ → ℝ → ℝ) (hf : ∀ (k : ℕ), ∀ x ∈ I.interval, HasDerivWithinAt (f k) (f (k + 1) x) I.interval x) (hg : ∀ (k : ℕ), ∀ x ∈ I.interval, HasDerivWithinAt (g k) (g (k + 1) x) I.interval x) (m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : HasDerivWithinAt (fun (y : ℝ) => leibnizSum (fun (k : ℕ) => f k y) (fun (k : ℕ) => g k y) m) (leibnizSum (fun (k : ℕ) => f k x) (fun (k : ℕ) => g k x) (m + 1)) I.interval x

Genuine first derivatives of the finite Leibniz sum reproduce the next jet.

@[reducible, inline]

noncomputable abbrev NavierStokes.AxisOperators.inputJet (I : AxisCoefficientSpace.Window) (ε : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) : ℝ → ℝ

Actual compatible input jets, with the indices in coefficient-first order.

Equations

• NavierStokes.AxisOperators.inputJet I ε A n m = NavierStokes.AxisCoefficientSpace.jet I (NavierStokes.AxisWeightEstimates.weight ε) (↑A) n m

theorem NavierStokes.AxisOperators.inputJet_bound (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) (x : ℝ) : |inputJet I ε A n m x| ≤ ‖A‖ * AxisWeightEstimates.weight ε n m

noncomputable def NavierStokes.AxisOperators.productFamily (I : AxisCoefficientSpace.Window) (ε : ℝ) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) (x : ℝ) : ℝ

Product jets are finite radial convolutions of the actual Leibniz sums.

Equations

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

theorem NavierStokes.AxisOperators.productFamily_eq (I : AxisCoefficientSpace.Window) (ε : ℝ) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) (x : ℝ) : productFamily I ε A B n m x = ∑ ij ∈ Finset.antidiagonal n, leibnizSum (fun (k : ℕ) => inputJet I ε A ij.1 k x) (fun (l : ℕ) => inputJet I ε B ij.2 l x) m

theorem NavierStokes.AxisOperators.productFamily_continuous (I : AxisCoefficientSpace.Window) (ε : ℝ) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) : ContinuousOn (productFamily I ε A B n m) I.interval

theorem NavierStokes.AxisOperators.productFamily_deriv (I : AxisCoefficientSpace.Window) (ε : ℝ) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) (x : ℝ) (hx : x ∈ I.interval) : HasDerivWithinAt (productFamily I ε A B n m) (productFamily I ε A B n (m + 1) x) I.interval x

theorem NavierStokes.AxisOperators.productFamily_bound (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) (x : ℝ) : |productFamily I ε A B n m x| ≤ 64 * ‖A‖ * ‖B‖ * AxisWeightEstimates.weight ε n m

structure NavierStokes.AxisOperators.BoundedLinearJetFamily (I : AxisCoefficientSpace.Window) (ε : ℝ) : Type

Data for a genuine linear operation on compatible coefficient jets.

• value : ↥(AxisCoefficientSpace.AxisSpace I ε) → ℕ → ℕ → ℝ → ℝ

  Value of BoundedLinearJetFamily, of type AxisSpace I ε → ℕ → ℕ → ℝ → ℝ.

• boundConstant : ℝ

  Bound constant of BoundedLinearJetFamily, of type ℝ.

• bound_nonneg : 0 ≤ self.boundConstant
• cont (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) : ContinuousOn (self.value A n m) I.interval
• deriv (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) (x : ℝ) : x ∈ I.interval → HasDerivWithinAt (self.value A n m) (self.value A n (m + 1) x) I.interval x
• add (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) (x : ℝ) : self.value (A + B) n m x = self.value A n m x + self.value B n m x
• smul (c : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) (x : ℝ) : self.value (c • A) n m x = c * self.value A n m x
• bound (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) (x : ℝ) : x ∈ I.interval → |self.value A n m x| ≤ self.boundConstant * ‖A‖ * AxisWeightEstimates.weight ε n m

noncomputable def NavierStokes.AxisOperators.linearValue (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (F : BoundedLinearJetFamily I ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) : ↥(AxisCoefficientSpace.AxisSpace I ε)

Linear value, constructed using ofJetFamily.

Equations

• NavierStokes.AxisOperators.linearValue I hε F A = NavierStokes.AxisCoefficientSpace.ofJetFamily I (NavierStokes.AxisWeightEstimates.weight ε) ⋯ (F.value A) ⋯ ⋯ (F.boundConstant * ‖A‖) ⋯ ⋯

theorem NavierStokes.AxisOperators.jet_linearValue (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (F : BoundedLinearJetFamily I ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : inputJet I ε (linearValue I hε F A) n m x = F.value A n m x

theorem NavierStokes.AxisOperators.norm_linearValue_le (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (F : BoundedLinearJetFamily I ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) : ‖linearValue I hε F A‖ ≤ F.boundConstant * ‖A‖

noncomputable def NavierStokes.AxisOperators.linearValueMap (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (F : BoundedLinearJetFamily I ε) : ↥(AxisCoefficientSpace.AxisSpace I ε) →ₗ[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε)

Linear value map, bundling toFun, map_add, apply, map_smul and the required compatibility proofs.

Equations

• NavierStokes.AxisOperators.linearValueMap I hε F = { toFun := NavierStokes.AxisOperators.linearValue I hε F, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def NavierStokes.AxisOperators.linearLift (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (F : BoundedLinearJetFamily I ε) : ↥(AxisCoefficientSpace.AxisSpace I ε) →L[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε)

Linear lift, given by (linearValueMap I hε F).mkContinuous F.boundConstant (norm_linearValue_le I hε F).

Equations

• NavierStokes.AxisOperators.linearLift I hε F = (NavierStokes.AxisOperators.linearValueMap I hε F).mkContinuous F.boundConstant ⋯

theorem NavierStokes.AxisOperators.jet_linearLift (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (F : BoundedLinearJetFamily I ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : inputJet I ε ((linearLift I hε F) A) n m x = F.value A n m x

theorem NavierStokes.AxisOperators.norm_linearLift_le (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (F : BoundedLinearJetFamily I ε) : ‖linearLift I hε F‖ ≤ F.boundConstant

structure NavierStokes.AxisOperators.BoundedBilinearJetFamily (I : AxisCoefficientSpace.Window) (ε : ℝ) : Type

Data for a genuine bilinear operation, including its derivative compatibility.

• value : ↥(AxisCoefficientSpace.AxisSpace I ε) → ↥(AxisCoefficientSpace.AxisSpace I ε) → ℕ → ℕ → ℝ → ℝ

  Value of BoundedBilinearJetFamily, of type AxisSpace I ε → AxisSpace I ε → ℕ → ℕ → ℝ → ℝ.

• boundConstant : ℝ

  Bound constant of BoundedBilinearJetFamily, of type ℝ.

• bound_nonneg : 0 ≤ self.boundConstant
• cont (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) : ContinuousOn (self.value A B n m) I.interval
• deriv (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) (x : ℝ) : x ∈ I.interval → HasDerivWithinAt (self.value A B n m) (self.value A B n (m + 1) x) I.interval x
• add_left (A B C : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) (x : ℝ) : self.value (A + B) C n m x = self.value A C n m x + self.value B C n m x
• smul_left (c : ℝ) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) (x : ℝ) : self.value (c • A) B n m x = c * self.value A B n m x
• add_right (A B C : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) (x : ℝ) : self.value A (B + C) n m x = self.value A B n m x + self.value A C n m x
• smul_right (c : ℝ) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) (x : ℝ) : self.value A (c • B) n m x = c * self.value A B n m x
• bound (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) (x : ℝ) : x ∈ I.interval → |self.value A B n m x| ≤ self.boundConstant * ‖A‖ * ‖B‖ * AxisWeightEstimates.weight ε n m

noncomputable def NavierStokes.AxisOperators.bilinearValue (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (F : BoundedBilinearJetFamily I ε) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) : ↥(AxisCoefficientSpace.AxisSpace I ε)

Bilinear value, constructed using ofJetFamily.

Equations

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

theorem NavierStokes.AxisOperators.jet_bilinearValue (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (F : BoundedBilinearJetFamily I ε) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : inputJet I ε (bilinearValue I hε F A B) n m x = F.value A B n m x

theorem NavierStokes.AxisOperators.norm_bilinearValue_le (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (F : BoundedBilinearJetFamily I ε) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) : ‖bilinearValue I hε F A B‖ ≤ F.boundConstant * ‖A‖ * ‖B‖

noncomputable def NavierStokes.AxisOperators.bilinearValueMap (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (F : BoundedBilinearJetFamily I ε) : ↥(AxisCoefficientSpace.AxisSpace I ε) →ₗ[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε) →ₗ[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε)

Bilinear value map, constructed using LinearMap.mk₂.

Equations

• NavierStokes.AxisOperators.bilinearValueMap I hε F = LinearMap.mk₂ ℝ (NavierStokes.AxisOperators.bilinearValue I hε F) ⋯ ⋯ ⋯ ⋯

noncomputable def NavierStokes.AxisOperators.bilinearLift (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (F : BoundedBilinearJetFamily I ε) : ↥(AxisCoefficientSpace.AxisSpace I ε) →L[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε) →L[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε)

Bilinear lift, given by (bilinearValueMap I hε F).mkContinuous₂ F.boundConstant (norm_bilinearValue_le I hε F).

Equations

• NavierStokes.AxisOperators.bilinearLift I hε F = (NavierStokes.AxisOperators.bilinearValueMap I hε F).mkContinuous₂ F.boundConstant ⋯

theorem NavierStokes.AxisOperators.jet_bilinearLift (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (F : BoundedBilinearJetFamily I ε) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : inputJet I ε (((bilinearLift I hε F) A) B) n m x = F.value A B n m x

theorem NavierStokes.AxisOperators.norm_bilinearLift_le (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (F : BoundedBilinearJetFamily I ε) : ‖bilinearLift I hε F‖ ≤ F.boundConstant

noncomputable def NavierStokes.AxisOperators.productData (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) : BoundedBilinearJetFamily I ε

Product data, bundling value, boundConstant, bound_nonneg, cont and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.AxisOperators.product (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) : ↥(AxisCoefficientSpace.AxisSpace I ε) →L[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε) →L[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε)

Actual continuous bilinear multiplication of coefficient functions.

Equations

• NavierStokes.AxisOperators.product I hε = NavierStokes.AxisOperators.bilinearLift I hε (NavierStokes.AxisOperators.productData I hε)

theorem NavierStokes.AxisOperators.norm_product_le (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) : ‖product I hε‖ ≤ 64

theorem NavierStokes.AxisOperators.jet_product (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : inputJet I ε (((product I hε) A) B) n m x = AxisWeightEstimates.jetProduct (fun (i k : ℕ) => inputJet I ε A i k x) (fun (j l : ℕ) => inputJet I ε B j l x) n m

theorem NavierStokes.AxisOperators.coefficient_product (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n : ℕ) {x : ℝ} (hx : x ∈ I.interval) : AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) (((product I hε) A) B) n x = ∑ ij ∈ Finset.antidiagonal n, AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) A ij.1 x * AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) B ij.2 x

noncomputable def NavierStokes.AxisOperators.rowData (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (c : ℕ → ℝ) (source : ℕ → ℕ) (offset : ℕ) (K : ℝ) (hK : 0 ≤ K) (hweight : ∀ (n m : ℕ), |c n| * AxisWeightEstimates.weight ε (source n) (offset + m) ≤ K * AxisWeightEstimates.weight ε n m) : BoundedLinearJetFamily I ε

A scalar multiple of a shifted coefficient/derivative row. This generic construction is instantiated below with explicit verified weight bounds.

Equations

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

noncomputable def NavierStokes.AxisOperators.primitiveScale : ℕ → ℝ

Primitive scale as an element of ℕ → ℝ | 0 => 0 | n + 1 => 1 / ((n : ℝ) + 1).

Equations

• NavierStokes.AxisOperators.primitiveScale 0 = 0
• NavierStokes.AxisOperators.primitiveScale n.succ = 1 / (↑n + 1)

noncomputable def NavierStokes.AxisOperators.inverseScale (r : ℕ) : ℕ → ℝ

Inverse scale as an element of ℕ → ℝ | 0 => 0 | n + 1 => 1 / radialDivisor r n.

Equations

• NavierStokes.AxisOperators.inverseScale r 0 = 0
• NavierStokes.AxisOperators.inverseScale r n.succ = 1 / NavierStokes.AxisWeightEstimates.radialDivisor r n

def NavierStokes.AxisOperators.multiplyYScale : ℕ → ℝ

Multiply Y scale as an element of ℕ → ℝ | 0 => 0 | _ + 1 => 1.

Equations

• NavierStokes.AxisOperators.multiplyYScale 0 = 0
• NavierStokes.AxisOperators.multiplyYScale n.succ = 1

theorem NavierStokes.AxisOperators.average_row_bound {ε : ℝ} (hε : 0 < ε) (n m : ℕ) : |1 / (↑n + 1)| * AxisWeightEstimates.weight ε n (0 + m) ≤ 1 * AxisWeightEstimates.weight ε n m

theorem NavierStokes.AxisOperators.primitive_row_bound {ε : ℝ} (hε : 0 < ε) (n m : ℕ) : |primitiveScale n| * AxisWeightEstimates.weight ε n.pred (0 + m) ≤ 80 * AxisWeightEstimates.weight ε n m

theorem NavierStokes.AxisOperators.inverse_row_bound {ε : ℝ} (hε : 0 < ε) {r : ℕ} (hr : 1 ≤ r) (n m : ℕ) : |inverseScale r n| * AxisWeightEstimates.weight ε n.pred (0 + m) ≤ 80 * AxisWeightEstimates.weight ε n m

theorem NavierStokes.AxisOperators.parameter_primitive_row_bound {ε : ℝ} (hε : 0 < ε) (n m : ℕ) : |primitiveScale n| * AxisWeightEstimates.weight ε n.pred (1 + m) ≤ 80 / ε * AxisWeightEstimates.weight ε n m

theorem NavierStokes.AxisOperators.multiplyY_row_bound {ε : ℝ} (hε : 0 < ε) (n m : ℕ) : |multiplyYScale n| * AxisWeightEstimates.weight ε n.pred (0 + m) ≤ 80 * AxisWeightEstimates.weight ε n m

noncomputable def NavierStokes.AxisOperators.averageData (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) : BoundedLinearJetFamily I ε

Average data, given by rowData I hε (fun n => 1 / ((n : ℝ) + 1)) id 0 1 (by norm_num) (average_row_bound hε).

Equations

• NavierStokes.AxisOperators.averageData I hε = NavierStokes.AxisOperators.rowData I hε (fun (n : ℕ) => 1 / (↑n + 1)) id 0 1 NavierStokes.AxisOperators.averageData._proof_1 ⋯

noncomputable def NavierStokes.AxisOperators.primitiveData (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) : BoundedLinearJetFamily I ε

Primitive data, given by rowData I hε primitiveScale Nat.pred 0 80 (by norm_num) (primitive_row_bound hε).

Equations

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

noncomputable def NavierStokes.AxisOperators.inverseData (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) : BoundedLinearJetFamily I ε

Inverse data, given by rowData I hε (inverseScale r) Nat.pred 0 80 (by norm_num) (inverse_row_bound hε hr).

Equations

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

noncomputable def NavierStokes.AxisOperators.parameterPrimitiveData (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) : BoundedLinearJetFamily I ε

Parameter primitive data, given by rowData I hε primitiveScale Nat.pred 1 (80 / ε) (by positivity) (parameter_primitive_row_bound hε).

Equations

• NavierStokes.AxisOperators.parameterPrimitiveData I hε = NavierStokes.AxisOperators.rowData I hε NavierStokes.AxisOperators.primitiveScale Nat.pred 1 (80 / ε) ⋯ ⋯

noncomputable def NavierStokes.AxisOperators.multiplyYData (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) : BoundedLinearJetFamily I ε

Multiply Y data, given by rowData I hε multiplyYScale Nat.pred 0 80 (by norm_num) (multiplyY_row_bound hε).

Equations

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

noncomputable def NavierStokes.AxisOperators.average (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) : ↥(AxisCoefficientSpace.AxisSpace I ε) →L[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε)

Average, given by linearLift I hε (averageData I hε).

Equations

• NavierStokes.AxisOperators.average I hε = NavierStokes.AxisOperators.linearLift I hε (NavierStokes.AxisOperators.averageData I hε)

noncomputable def NavierStokes.AxisOperators.primitive (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) : ↥(AxisCoefficientSpace.AxisSpace I ε) →L[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε)

Primitive, given by linearLift I hε (primitiveData I hε).

Equations

• NavierStokes.AxisOperators.primitive I hε = NavierStokes.AxisOperators.linearLift I hε (NavierStokes.AxisOperators.primitiveData I hε)

noncomputable def NavierStokes.AxisOperators.regularInverse (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) : ↥(AxisCoefficientSpace.AxisSpace I ε) →L[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε)

Regular inverse, given by linearLift I hε (inverseData I hε r hr).

Equations

• NavierStokes.AxisOperators.regularInverse I hε r hr = NavierStokes.AxisOperators.linearLift I hε (NavierStokes.AxisOperators.inverseData I hε r hr)

noncomputable def NavierStokes.AxisOperators.parameterPrimitive (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) : ↥(AxisCoefficientSpace.AxisSpace I ε) →L[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε)

Parameter primitive, given by linearLift I hε (parameterPrimitiveData I hε).

Equations

• NavierStokes.AxisOperators.parameterPrimitive I hε = NavierStokes.AxisOperators.linearLift I hε (NavierStokes.AxisOperators.parameterPrimitiveData I hε)

noncomputable def NavierStokes.AxisOperators.mulY (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) : ↥(AxisCoefficientSpace.AxisSpace I ε) →L[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε)

Mul Y, given by linearLift I hε (multiplyYData I hε).

Equations

• NavierStokes.AxisOperators.mulY I hε = NavierStokes.AxisOperators.linearLift I hε (NavierStokes.AxisOperators.multiplyYData I hε)

theorem NavierStokes.AxisOperators.norm_average_le (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) : ‖average I hε‖ ≤ 1

theorem NavierStokes.AxisOperators.norm_primitive_le (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) : ‖primitive I hε‖ ≤ 80

theorem NavierStokes.AxisOperators.norm_regularInverse_le (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) : ‖regularInverse I hε r hr‖ ≤ 80

theorem NavierStokes.AxisOperators.norm_parameterPrimitive_le (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) : ‖parameterPrimitive I hε‖ ≤ 80 / ε

theorem NavierStokes.AxisOperators.norm_mulY_le (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) : ‖mulY I hε‖ ≤ 80

theorem NavierStokes.AxisOperators.jet_regularInverse_zero (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : inputJet I ε ((regularInverse I hε r hr) A) 0 m x = 0

theorem NavierStokes.AxisOperators.jet_regularInverse_succ (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : inputJet I ε ((regularInverse I hε r hr) A) (n + 1) m x = inputJet I ε A n m x / AxisWeightEstimates.radialDivisor r n

noncomputable def NavierStokes.AxisOperators.differentialFamily (I : AxisCoefficientSpace.Window) (ε : ℝ) (r p : ℕ) (d : ℕ → ℝ) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) : ℕ → ℕ → ℝ → ℝ

A radial inverse applied to a finite product with a fixed parameter shift on the first factor and radial multiplier d on the second.

Equations

• One or more equations did not get rendered due to their size.
• NavierStokes.AxisOperators.differentialFamily I ε r p d A B 0 x✝¹ x✝ = 0

theorem NavierStokes.AxisOperators.differentialFamily_succ_eq (I : AxisCoefficientSpace.Window) (ε : ℝ) (r p : ℕ) (d : ℕ → ℝ) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) (x : ℝ) : differentialFamily I ε r p d A B (n + 1) m x = ∑ ij ∈ Finset.antidiagonal n, d ij.2 / AxisWeightEstimates.radialDivisor r n * leibnizSum (fun (k : ℕ) => inputJet I ε A ij.1 (p + k) x) (fun (l : ℕ) => inputJet I ε B ij.2 l x) m

theorem NavierStokes.AxisOperators.differentialFamily_continuous (I : AxisCoefficientSpace.Window) (ε : ℝ) (r p : ℕ) (d : ℕ → ℝ) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) : ContinuousOn (differentialFamily I ε r p d A B n m) I.interval

theorem NavierStokes.AxisOperators.differentialFamily_deriv (I : AxisCoefficientSpace.Window) (ε : ℝ) (r p : ℕ) (d : ℕ → ℝ) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) (x : ℝ) (hx : x ∈ I.interval) : HasDerivWithinAt (differentialFamily I ε r p d A B n m) (differentialFamily I ε r p d A B n (m + 1) x) I.interval x

theorem NavierStokes.AxisOperators.shifted_kernel_weight_le (D d a b C w w' v : ℝ) (hD : 0 < D) (hd : 0 ≤ d) (ha : 0 ≤ a) (_hb : 0 ≤ b) (hC : 0 ≤ C) (hw' : 0 ≤ w') (hv : 0 ≤ v) (hshift : w ≤ C * b * w') (hfactor : b * d ≤ D) : d / D * a * w * v ≤ C * (a * w' * v)

theorem NavierStokes.AxisOperators.differentialFamily_bound (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r p : ℕ) (hr : 1 ≤ r) (d b : ℕ → ℝ) (C : ℝ) (hd : ∀ (j : ℕ), 0 ≤ d j) (hb : ∀ (i : ℕ), 0 ≤ b i) (hC : 0 ≤ C) (hshift : ∀ (i k : ℕ), AxisWeightEstimates.weight ε i (p + k) ≤ C * b i * AxisWeightEstimates.weight ε (i + 1) k) (hfactor : ∀ (n i j : ℕ), i + j = n → b i * d j ≤ AxisWeightEstimates.radialDivisor r n) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) (x : ℝ) : |differentialFamily I ε r p d A B n m x| ≤ 64 * C * ‖A‖ * ‖B‖ * AxisWeightEstimates.weight ε n m

The mixed estimate is proved with the derivative shift and the radial inverse together; the separate derivative need not be bounded.

noncomputable def NavierStokes.AxisOperators.differentialData (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r p : ℕ) (hr : 1 ≤ r) (d b : ℕ → ℝ) (C : ℝ) (hd : ∀ (j : ℕ), 0 ≤ d j) (hb : ∀ (i : ℕ), 0 ≤ b i) (hC : 0 ≤ C) (hshift : ∀ (i k : ℕ), AxisWeightEstimates.weight ε i (p + k) ≤ C * b i * AxisWeightEstimates.weight ε (i + 1) k) (hfactor : ∀ (n i j : ℕ), i + j = n → b i * d j ≤ AxisWeightEstimates.radialDivisor r n) : BoundedBilinearJetFamily I ε

Differential data, bundling value, boundConstant, bound_nonneg, cont and the required compatibility proofs.

Equations

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

theorem NavierStokes.AxisOperators.radial_index_le_divisor {r : ℕ} (hr : 1 ≤ r) (n : ℕ) : ↑n + 1 ≤ AxisWeightEstimates.radialDivisor r n

noncomputable def NavierStokes.AxisOperators.inverseMixedData (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) : BoundedBilinearJetFamily I ε

Inverse mixed data, constructed using differentialData.

Equations

• NavierStokes.AxisOperators.inverseMixedData I hε r hr = NavierStokes.AxisOperators.differentialData I hε r 1 hr (fun (j : ℕ) => ↑j) (fun (i : ℕ) => ↑i + 1) (80 / ε) ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable def NavierStokes.AxisOperators.inverseParamProductData (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) : BoundedBilinearJetFamily I ε

Inverse param product data, constructed using differentialData.

Equations

• NavierStokes.AxisOperators.inverseParamProductData I hε r hr = NavierStokes.AxisOperators.differentialData I hε r 1 hr (fun (x : ℕ) => 1) (fun (i : ℕ) => ↑i + 1) (80 / ε) ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable def NavierStokes.AxisOperators.inverseDotProductData (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) : BoundedBilinearJetFamily I ε

Inverse dot product data, constructed using differentialData.

Equations

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

noncomputable def NavierStokes.AxisOperators.inverseMixed (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) : ↥(AxisCoefficientSpace.AxisSpace I ε) →L[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε) →L[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε)

J_r ((∂η f) D_Y g), formed and estimated without either unbounded derivative as a standalone operator on the coefficient space.

Equations

• NavierStokes.AxisOperators.inverseMixed I hε r hr = NavierStokes.AxisOperators.bilinearLift I hε (NavierStokes.AxisOperators.inverseMixedData I hε r hr)

noncomputable def NavierStokes.AxisOperators.inverseParamProduct (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) : ↥(AxisCoefficientSpace.AxisSpace I ε) →L[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε) →L[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε)

J_r ((∂η f) g) with the parameter derivative on the first argument.

Equations

• NavierStokes.AxisOperators.inverseParamProduct I hε r hr = NavierStokes.AxisOperators.bilinearLift I hε (NavierStokes.AxisOperators.inverseParamProductData I hε r hr)

noncomputable def NavierStokes.AxisOperators.inverseDotProduct (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) : ↥(AxisCoefficientSpace.AxisSpace I ε) →L[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε) →L[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε)

J_r (f D_Y g) with the radial dot on the second argument.

Equations

• NavierStokes.AxisOperators.inverseDotProduct I hε r hr = NavierStokes.AxisOperators.bilinearLift I hε (NavierStokes.AxisOperators.inverseDotProductData I hε r hr)

theorem NavierStokes.AxisOperators.norm_inverseMixed_le (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) : ‖inverseMixed I hε r hr‖ ≤ 5120 / ε

theorem NavierStokes.AxisOperators.norm_inverseParamProduct_le (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) : ‖inverseParamProduct I hε r hr‖ ≤ 5120 / ε

theorem NavierStokes.AxisOperators.norm_inverseDotProduct_le (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) : ‖inverseDotProduct I hε r hr‖ ≤ 5120

theorem NavierStokes.AxisOperators.jet_inverseMixed (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : inputJet I ε (((inverseMixed I hε r hr) A) B) n m x = differentialFamily I ε r 1 (fun (j : ℕ) => ↑j) A B n m x

theorem NavierStokes.AxisOperators.jet_inverseParamProduct (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : inputJet I ε (((inverseParamProduct I hε r hr) A) B) n m x = differentialFamily I ε r 1 (fun (x : ℕ) => 1) A B n m x

theorem NavierStokes.AxisOperators.jet_inverseDotProduct (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : inputJet I ε (((inverseDotProduct I hε r hr) A) B) n m x = differentialFamily I ε r 0 (fun (j : ℕ) => ↑j) A B n m x

The nonlinear natural-axis fixed point

The local bounds below are computed from bounded linear and bilinear operations. In particular, the nonlinear remainders' Lipschitz estimates are conclusions, not assumptions.

The natural-axis resolvent from factorial decay of radial shifts

The inverse is constructed by a norm-convergent alternating series. No small-operator-norm hypothesis is used. The generic Banach-ring lemmas isolate the analytic implication of the factorial estimate from its radial proof.

@[instance_reducible]

noncomputable def NavierStokes.AxisResolvent.instAxisResolvent1 (I : AxisCoefficientSpace.Window) (ε : ℝ) : NormedAddCommGroup ↥(AxisCoefficientSpace.AxisSpace I ε)

Cache the standard NormedAddCommGroup (AxisCoefficientSpace.AxisSpace I ε) instance to shorten typeclass synthesis.

Equations

• NavierStokes.AxisResolvent.instAxisResolvent1 I ε = inferInstance

@[instance_reducible]

noncomputable def NavierStokes.AxisResolvent.instAxisResolvent2 (I : AxisCoefficientSpace.Window) (ε : ℝ) : NormedSpace ℝ ↥(AxisCoefficientSpace.AxisSpace I ε)

Cache the standard NormedSpace ℝ (AxisCoefficientSpace.AxisSpace I ε) instance to shorten typeclass synthesis.

Equations

• NavierStokes.AxisResolvent.instAxisResolvent2 I ε = inferInstance

noncomputable def NavierStokes.AxisResolvent.factorialMajorant (K : ℝ) (k : ℕ) : ℝ

The majorant produced by k applications of the regular radial inverse.

Equations

• NavierStokes.AxisResolvent.factorialMajorant K k = K ^ k / (↑k.factorial * ↑(k + 1).factorial)

theorem NavierStokes.AxisResolvent.factorialMajorant_nonneg {K : ℝ} (hK : 0 ≤ K) (k : ℕ) : 0 ≤ factorialMajorant K k

theorem NavierStokes.AxisResolvent.factorialMajorant_le_exp_term {K : ℝ} (hK : 0 ≤ K) (k : ℕ) : factorialMajorant K k ≤ K ^ k / ↑k.factorial

theorem NavierStokes.AxisResolvent.summable_factorialMajorant {K : ℝ} (hK : 0 ≤ K) : Summable (factorialMajorant K)

@[simp]

theorem NavierStokes.AxisResolvent.factorialMajorant_zero (K : ℝ) : factorialMajorant K 0 = 1

theorem NavierStokes.AxisResolvent.factorialMajorant_succ (K : ℝ) (k : ℕ) : factorialMajorant K (k + 1) = K / ((↑k + 1) * (↑k + 2)) * factorialMajorant K k

def NavierStokes.AxisResolvent.JetVanishesBelow (f : ℕ → ℕ → ℝ) (k : ℕ) : Prop

All parameter jets below a prescribed radial degree vanish.

Equations

• NavierStokes.AxisResolvent.JetVanishesBelow f k = ∀ n < k, ∀ (m : ℕ), f n m = 0

theorem NavierStokes.AxisResolvent.jetProduct_vanishesBelow_right (f g : ℕ → ℕ → ℝ) (k : ℕ) (hg : JetVanishesBelow g k) : JetVanishesBelow (AxisWeightEstimates.jetProduct f g) k

theorem NavierStokes.AxisResolvent.regularInverseJet_vanishesBelow (f : ℕ → ℕ → ℝ) (k : ℕ) (hf : JetVanishesBelow f k) : JetVanishesBelow (AxisWeightEstimates.regularInverseJet 2 f) (k + 1)

theorem NavierStokes.AxisResolvent.radialDivisor_two_mono {k n : ℕ} (hkn : k ≤ n) : AxisWeightEstimates.radialDivisor 2 k ≤ AxisWeightEstimates.radialDivisor 2 n

theorem NavierStokes.AxisResolvent.regularInverseJet_bound_on_order {ε F : ℝ} (hε : 0 < ε) (hF : 0 ≤ F) (f : ℕ → ℕ → ℝ) (k : ℕ) (hz : JetVanishesBelow f k) (hf : ∀ (n m : ℕ), |f n m| ≤ F * AxisWeightEstimates.weight ε n m) (n m : ℕ) : |AxisWeightEstimates.regularInverseJet 2 f n m| ≤ 80 / AxisWeightEstimates.radialDivisor 2 k * F * AxisWeightEstimates.weight ε n m

A radial inverse has a better norm bound on profiles whose first k radial coefficients vanish. This is the source of the two factorials.

theorem NavierStokes.AxisResolvent.norm_neg_pow_eq {R : Type u_1} [NormedRing R] (Q : R) (k : ℕ) : ‖(-Q) ^ k‖ = ‖Q ^ k‖

noncomputable def NavierStokes.AxisResolvent.alternatingResolvent {R : Type u_1} [NormedRing R] (Q : R) : R

The alternating series itself, as an element of the ambient Banach ring.

Equations

• NavierStokes.AxisResolvent.alternatingResolvent Q = ∑' (k : ℕ), (-Q) ^ k

theorem NavierStokes.AxisResolvent.one_sub_mul_tsum_pow {R : Type u_1} [NormedRing R] {Q : R} (hs : Summable fun (k : ℕ) => Q ^ k) : (1 - Q) * ∑' (k : ℕ), Q ^ k = 1

A summable geometric family gives an exact left inverse, even when the norm of its ratio is not less than one.

theorem NavierStokes.AxisResolvent.tsum_pow_mul_one_sub {R : Type u_1} [NormedRing R] {Q : R} (hs : Summable fun (k : ℕ) => Q ^ k) : (∑' (k : ℕ), Q ^ k) * (1 - Q) = 1

The same convergent series is also a right inverse in a possibly noncommutative ring.

theorem NavierStokes.AxisResolvent.summable_norm_neg_pow_of_factorial_bound {R : Type u_1} [NormedRing R] (Q : R) {K : ℝ} (hK : 0 ≤ K) (hQ : ∀ (k : ℕ), ‖Q ^ k‖ ≤ factorialMajorant K k) : Summable fun (k : ℕ) => ‖(-Q) ^ k‖

theorem NavierStokes.AxisResolvent.summable_neg_pow_of_factorial_bound {R : Type u_1} [NormedRing R] [CompleteSpace R] (Q : R) {K : ℝ} (hK : 0 ≤ K) (hQ : ∀ (k : ℕ), ‖Q ^ k‖ ≤ factorialMajorant K k) : Summable fun (k : ℕ) => (-Q) ^ k

theorem NavierStokes.AxisResolvent.hasSum_alternatingResolvent {R : Type u_1} [NormedRing R] [CompleteSpace R] (Q : R) {K : ℝ} (hK : 0 ≤ K) (hQ : ∀ (k : ℕ), ‖Q ^ k‖ ≤ factorialMajorant K k) : HasSum (fun (k : ℕ) => (-Q) ^ k) (alternatingResolvent Q)

theorem NavierStokes.AxisResolvent.one_add_mul_alternatingResolvent {R : Type u_1} [NormedRing R] [CompleteSpace R] (Q : R) {K : ℝ} (hK : 0 ≤ K) (hQ : ∀ (k : ℕ), ‖Q ^ k‖ ≤ factorialMajorant K k) : (1 + Q) * alternatingResolvent Q = 1

theorem NavierStokes.AxisResolvent.alternatingResolvent_mul_one_add {R : Type u_1} [NormedRing R] [CompleteSpace R] (Q : R) {K : ℝ} (hK : 0 ≤ K) (hQ : ∀ (k : ℕ), ‖Q ^ k‖ ≤ factorialMajorant K k) : alternatingResolvent Q * (1 + Q) = 1

theorem NavierStokes.AxisResolvent.norm_alternatingResolvent_le {R : Type u_1} [NormedRing R] (Q : R) {K : ℝ} (hK : 0 ≤ K) (hQ : ∀ (k : ℕ), ‖Q ^ k‖ ≤ factorialMajorant K k) : ‖alternatingResolvent Q‖ ≤ ∑' (k : ℕ), factorialMajorant K k

theorem NavierStokes.AxisResolvent.pow_bound_of_filtration {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Q : E →L[ℝ] E) (P : ℕ → E → Prop) {K : ℝ} (hK : 0 ≤ K) (hzero : ∀ (x : E), P 0 x) (hstep : ∀ (k : ℕ) (x : E), P k x → P (k + 1) (Q x)) (hbound : ∀ (k : ℕ) (x : E), P k x → ‖Q x‖ ≤ K / ((↑k + 1) * (↑k + 2)) * ‖x‖) (k : ℕ) : ‖Q ^ k‖ ≤ factorialMajorant K k

Iteration through the radial-degree filtration gives a factorial bound for the actual operator powers. No bound less than one is assumed.

theorem NavierStokes.AxisResolvent.one_add_apply_alternatingResolvent {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (Q : E →L[ℝ] E) {K : ℝ} (hK : 0 ≤ K) (hQ : ∀ (k : ℕ), ‖Q ^ k‖ ≤ factorialMajorant K k) (x : E) : (1 + Q) ((alternatingResolvent Q) x) = x

Pointwise form of the inverse equation used in the nonlinear fixed-point map.

theorem NavierStokes.AxisResolvent.alternatingResolvent_apply_one_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (Q : E →L[ℝ] E) {K : ℝ} (hK : 0 ≤ K) (hQ : ∀ (k : ℕ), ‖Q ^ k‖ ≤ factorialMajorant K k) (x : E) : (alternatingResolvent Q) ((1 + Q) x) = x

theorem NavierStokes.AxisResolvent.alternatingResolvent_equation {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (Q : E →L[ℝ] E) {K : ℝ} (hK : 0 ≤ K) (hQ : ∀ (k : ℕ), ‖Q ^ k‖ ≤ factorialMajorant K k) (x : E) : (alternatingResolvent Q) x + Q ((alternatingResolvent Q) x) = x

theorem NavierStokes.AxisResolvent.alternatingResolvent_unique {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (Q : E →L[ℝ] E) {K : ℝ} (hK : 0 ≤ K) (hQ : ∀ (k : ℕ), ‖Q ^ k‖ ≤ factorialMajorant K k) {x b : E} (hx : x + Q x = b) : x = (alternatingResolvent Q) b

The inverse gives the unique solution of the integrated linear equation.

noncomputable def NavierStokes.AxisResolvent.oneAddEquiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (Q : E →L[ℝ] E) {K : ℝ} (hK : 0 ≤ K) (hQ : ∀ (k : ℕ), ‖Q ^ k‖ ≤ factorialMajorant K k) : E ≃L[ℝ] E

Both continuous directions are constructed explicitly from the series.

Equations

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

def NavierStokes.AxisResolvent.AxisVanishesBelow (I : AxisCoefficientSpace.Window) (ε : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k : ℕ) : Prop

Radial order in the actual compatible coefficient space.

Equations

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

theorem NavierStokes.AxisResolvent.axis_abs_jet_le (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) (x : ℝ) : |AxisCoefficientSpace.jet I (AxisWeightEstimates.weight ε) (↑A) n m x| ≤ ‖A‖ * AxisWeightEstimates.weight ε n m

theorem NavierStokes.AxisResolvent.axis_norm_le_of_jet_bound (I : AxisCoefficientSpace.Window) {ε C : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (hC : 0 ≤ C) (hA : ∀ (n m : ℕ) (x : ↑I.interval), |AxisCoefficientSpace.jet I (AxisWeightEstimates.weight ε) (↑A) n m ↑x| ≤ C * AxisWeightEstimates.weight ε n m) : ‖A‖ ≤ C

def NavierStokes.AxisResolvent.IsAxisLinearOperator (I : AxisCoefficientSpace.Window) (ε : ℝ) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (Q : ↥(AxisCoefficientSpace.AxisSpace I ε) →L[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε)) : Prop

The concrete jet identity for (1/2) J₂ Mχ. This records the operation, not any inverse or spectral property. It allows the estimate to be applied to any compatible construction of the two bounded operators.

Equations

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

theorem NavierStokes.AxisResolvent.axisLinearOperator_increases_order (I : AxisCoefficientSpace.Window) {ε : ℝ} (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (Q : ↥(AxisCoefficientSpace.AxisSpace I ε) →L[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε)) (hQ : IsAxisLinearOperator I ε χ Q) (k : ℕ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (hA : AxisVanishesBelow I ε A k) : AxisVanishesBelow I ε (Q A) (k + 1)

theorem NavierStokes.AxisResolvent.axisLinearOperator_bound_on_order (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (Q : ↥(AxisCoefficientSpace.AxisSpace I ε) →L[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε)) (hQ : IsAxisLinearOperator I ε χ Q) (k : ℕ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (hA : AxisVanishesBelow I ε A k) : ‖Q A‖ ≤ 2560 * ‖χ‖ / AxisWeightEstimates.radialDivisor 2 k * ‖A‖

theorem NavierStokes.AxisResolvent.axisLinearOperator_pow_bound (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (Q : ↥(AxisCoefficientSpace.AxisSpace I ε) →L[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε)) (hQ : IsAxisLinearOperator I ε χ Q) (k : ℕ) : ‖Q ^ k‖ ≤ factorialMajorant (2560 * ‖χ‖) k

The actual weighted radial estimate: any operator with the stated (1/2) J₂ Mχ coefficients has factorial-decaying powers. The multiplier may even depend on the radial variable; the natural-axis multiplier is a special case.

theorem NavierStokes.AxisResolvent.axisLinearOperator_resolvent_equation (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (Q : ↥(AxisCoefficientSpace.AxisSpace I ε) →L[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε)) (hQ : IsAxisLinearOperator I ε χ Q) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) : (alternatingResolvent Q) A + Q ((alternatingResolvent Q) A) = A

noncomputable def NavierStokes.AxisResolvent.naturalOperator (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) : ↥(AxisCoefficientSpace.AxisSpace I ε) →L[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε)

The exact bounded operator in the natural angular equation.

Equations

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

theorem NavierStokes.AxisResolvent.naturalOperator_isAxisLinearOperator (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) : IsAxisLinearOperator I ε χ (naturalOperator I hε χ)

theorem NavierStokes.AxisResolvent.naturalOperator_pow_bound (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k : ℕ) : ‖naturalOperator I hε χ ^ k‖ ≤ factorialMajorant (2560 * ‖χ‖) k

The operator norm has factorial decay with an explicit constant.

noncomputable def NavierStokes.AxisResolvent.naturalResolvent (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) : ↥(AxisCoefficientSpace.AxisSpace I ε) →L[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε)

The linear resolvent used in the nonlinear natural-axis contraction.

Equations

• NavierStokes.AxisResolvent.naturalResolvent I hε χ = NavierStokes.AxisResolvent.alternatingResolvent (NavierStokes.AxisResolvent.naturalOperator I hε χ)

theorem NavierStokes.AxisResolvent.naturalResolvent_hasSum (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) : HasSum (fun (k : ℕ) => (-naturalOperator I hε χ) ^ k) (naturalResolvent I hε χ)

theorem NavierStokes.AxisResolvent.naturalResolvent_norm_le (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) : ‖naturalResolvent I hε χ‖ ≤ ∑' (k : ℕ), factorialMajorant (2560 * ‖χ‖) k

theorem NavierStokes.AxisResolvent.one_add_mul_naturalResolvent (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) : (1 + naturalOperator I hε χ) * naturalResolvent I hε χ = 1

theorem NavierStokes.AxisResolvent.naturalResolvent_mul_one_add (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) : naturalResolvent I hε χ * (1 + naturalOperator I hε χ) = 1

theorem NavierStokes.AxisResolvent.one_add_apply_naturalResolvent (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ A : ↥(AxisCoefficientSpace.AxisSpace I ε)) : (1 + naturalOperator I hε χ) ((naturalResolvent I hε χ) A) = A

theorem NavierStokes.AxisResolvent.naturalResolvent_apply_one_add (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ A : ↥(AxisCoefficientSpace.AxisSpace I ε)) : (naturalResolvent I hε χ) ((1 + naturalOperator I hε χ) A) = A

theorem NavierStokes.AxisResolvent.naturalResolvent_equation (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ A : ↥(AxisCoefficientSpace.AxisSpace I ε)) : (naturalResolvent I hε χ) A + (naturalOperator I hε χ) ((naturalResolvent I hε χ) A) = A

theorem NavierStokes.AxisResolvent.naturalResolvent_unique (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) {A b : ↥(AxisCoefficientSpace.AxisSpace I ε)} (hA : A + (naturalOperator I hε χ) A = b) : A = (naturalResolvent I hε χ) b

noncomputable def NavierStokes.AxisResolvent.naturalEquationEquiv (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) : ↥(AxisCoefficientSpace.AxisSpace I ε) ≃L[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε)

In particular, the reference angular profile is obtained by applying this map to the constant coefficient representing 1.

Equations

• NavierStokes.AxisResolvent.naturalEquationEquiv I hε χ = NavierStokes.AxisResolvent.oneAddEquiv (NavierStokes.AxisResolvent.naturalOperator I hε χ) ⋯ ⋯

structure NavierStokes.AxisContraction.Controlled (E : Type u_5) (F : Type u_6) [NormedAddCommGroup E] [NormedAddCommGroup F] (R : ℝ) : Type (max u_5 u_6)

A function with explicit bounds on a fixed norm ball.

• eval : E → F

  Eval of Controlled, of type E → F.

• bound : ℝ

  Bound of Controlled, of type ℝ.

• lip : ℝ

  Lip of Controlled, of type ℝ.

• bound_nonneg : 0 ≤ self.bound
• lip_nonneg : 0 ≤ self.lip
• norm_le (x : E) : ‖x‖ ≤ R → ‖self.eval x‖ ≤ self.bound
• sub_le (x y : E) : ‖x‖ ≤ R → ‖y‖ ≤ R → ‖self.eval x - self.eval y‖ ≤ self.lip * ‖x - y‖

noncomputable def NavierStokes.AxisContraction.Controlled.constBound {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {R : ℝ} (a : F) (B : ℝ) (hB : 0 ≤ B) (ha : ‖a‖ ≤ B) : Controlled E F R

Const bound, bundling eval, bound, lip, bound_nonneg and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.AxisContraction.Controlled.const {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {R : ℝ} (a : F) : Controlled E F R

Const, given by constBound a ‖a‖ (norm_nonneg a) le_rfl.

Equations

• NavierStokes.AxisContraction.Controlled.const a = NavierStokes.AxisContraction.Controlled.constBound a ‖a‖ ⋯ ⋯

noncomputable def NavierStokes.AxisContraction.Controlled.fst {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {R : ℝ} (hR : 0 ≤ R) : Controlled (E × F) E R

Fst, bundling eval, bound, lip, bound_nonneg and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.AxisContraction.Controlled.snd {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {R : ℝ} (hR : 0 ≤ R) : Controlled (E × F) F R

Snd, bundling eval, bound, lip, bound_nonneg and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.AxisContraction.Controlled.add {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {R : ℝ} (f g : Controlled E F R) : Controlled E F R

Add, bundling eval, bound, lip, bound_nonneg and the required compatibility proofs.

Equations

• f.add g = { eval := fun (x : E) => f.eval x + g.eval x, bound := f.bound + g.bound, lip := f.lip + g.lip, bound_nonneg := ⋯, lip_nonneg := ⋯, norm_le := ⋯, sub_le := ⋯ }

noncomputable def NavierStokes.AxisContraction.Controlled.neg {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {R : ℝ} (f : Controlled E F R) : Controlled E F R

Neg, bundling eval, bound, lip, bound_nonneg and the required compatibility proofs.

Equations

• f.neg = { eval := fun (x : E) => -f.eval x, bound := f.bound, lip := f.lip, bound_nonneg := ⋯, lip_nonneg := ⋯, norm_le := ⋯, sub_le := ⋯ }

noncomputable def NavierStokes.AxisContraction.Controlled.sub {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {R : ℝ} (f g : Controlled E F R) : Controlled E F R

Sub, given by add f (neg g).

Equations

• f.sub g = f.add g.neg

noncomputable def NavierStokes.AxisContraction.Controlled.unitSmul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] {R : ℝ} (c : ℝ) (hc : |c| ≤ 1) (f : Controlled E F R) : Controlled E F R

Scaling by a scalar of absolute value at most one keeps the same upper bounds, making the final bounds uniform in the parameter inverse.

Equations

• NavierStokes.AxisContraction.Controlled.unitSmul c hc f = { eval := fun (x : E) => c • f.eval x, bound := f.bound, lip := f.lip, bound_nonneg := ⋯, lip_nonneg := ⋯, norm_le := ⋯, sub_le := ⋯ }

noncomputable def NavierStokes.AxisContraction.Controlled.linear {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {R : ℝ} (L : F →L[ℝ] G) (f : Controlled E F R) : Controlled E G R

Linear, bundling eval, bound, lip, bound_nonneg and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.AxisContraction.Controlled.bilinear {E : Type u_1} {F : Type u_2} {G : Type u_3} {H : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedAddCommGroup H] [NormedSpace ℝ H] {R : ℝ} (B : F →L[ℝ] G →L[ℝ] H) (f : Controlled E F R) (g : Controlled E G R) : Controlled E H R

Bilinear, bundling eval, bound, lip, bound_nonneg and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.AxisContraction.Controlled.pair {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {R : ℝ} (f : Controlled E F R) (g : Controlled E G R) : Controlled E (F × G) R

Pair, bundling eval, bound, lip, bound_nonneg and the required compatibility proofs.

Equations

• f.pair g = { eval := fun (x : E) => (f.eval x, g.eval x), bound := f.bound + g.bound, lip := f.lip + g.lip, bound_nonneg := ⋯, lip_nonneg := ⋯, norm_le := ⋯, sub_le := ⋯ }

theorem NavierStokes.AxisContraction.exists_fixedPoint_of_controlled {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (x₀ : E) (f : Controlled E E (‖x₀‖ + 1)) (s : ℝ) (hs : 0 ≤ s) (hbound : s * f.bound ≤ 1) (hlip : s * f.lip ≤ 1 / 2) : ∃ (x : E), ‖x - x₀‖ ≤ 1 ∧ x₀ + s • f.eval x = x ∧ ‖x - x₀‖ ≤ s * f.bound ∧ ∀ (y : E), ‖y - x₀‖ ≤ 1 → x₀ + s • f.eval y = y → y = x

The complete-subset fixed point step used after constructing, rather than assuming, the remainder's local estimates.

structure NavierStokes.AxisContraction.NaturalOperators (V : Type u_5) [NormedAddCommGroup V] [NormedSpace ℝ V] : Type u_5

Actual bounded coefficient operators, later instantiated by AxisOperators. The derivative operators occur only after their regular radial inverses.

• product : V →L[ℝ] V →L[ℝ] V

  Product of NaturalOperators, of type V →L[ℝ] V →L[ℝ] V.

• average : V →L[ℝ] V

  Average of NaturalOperators, of type V →L[ℝ] V.

• primitive : V →L[ℝ] V

  Primitive of NaturalOperators, of type V →L[ℝ] V.

• parameterPrimitive : V →L[ℝ] V

  Parameter primitive of NaturalOperators, of type V →L[ℝ] V.

• mulY : V →L[ℝ] V

  Mul Y of NaturalOperators, of type V →L[ℝ] V.

• j1 : V →L[ℝ] V

  J1 of NaturalOperators, of type V →L[ℝ] V.

• j2 : V →L[ℝ] V

  J2 of NaturalOperators, of type V →L[ℝ] V.

• param1 : V →L[ℝ] V →L[ℝ] V

  Param1 of NaturalOperators, of type V →L[ℝ] V →L[ℝ] V.

• param2 : V →L[ℝ] V →L[ℝ] V

  Param2 of NaturalOperators, of type V →L[ℝ] V →L[ℝ] V.

• dot1 : V →L[ℝ] V →L[ℝ] V

  Dot1 of NaturalOperators, of type V →L[ℝ] V →L[ℝ] V.

• dot2 : V →L[ℝ] V →L[ℝ] V

  Dot2 of NaturalOperators, of type V →L[ℝ] V →L[ℝ] V.

• mixed1 : V →L[ℝ] V →L[ℝ] V

  Mixed1 of NaturalOperators, of type V →L[ℝ] V →L[ℝ] V.

• mixed2 : V →L[ℝ] V →L[ℝ] V

  Mixed2 of NaturalOperators, of type V →L[ℝ] V →L[ℝ] V.

structure NavierStokes.AxisContraction.AxisData (V : Type u_5) : Type u_5

Fixed analytic coefficient data. In the manuscript all entries have radial degree zero. The normalized gradient is ξ₀/Λ, independent of Λ.

• A : ℝ

  A of AxisData, of type ℝ.

• D : ℝ

  Domain data of AxisData, of type ℝ.

• h : ℝ

  Step-size parameter of AxisData, of type ℝ.

• one : V

  One of AxisData, of type V.

• eta : V

  Eta of AxisData, of type V.

• d : V

  D of AxisData, of type V.

• inverseL : V

  Inverse L of AxisData, of type V.

• uStar : V

  U star of AxisData, of type V.

• uStarEta : V

  U star eta of AxisData, of type V.

• wStar : V

  W star of AxisData, of type V.

• hStar : V

  H star of AxisData, of type V.

• normalizedGradient : V

  Normalized gradient of AxisData, of type V.

• zStar : V

  Z star of AxisData, of type V.

noncomputable def NavierStokes.AxisContraction.angularLinearCoefficient {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] (O : NaturalOperators V) (d : AxisData V) : V

Angular linear coefficient, given by d.wStar + d.h • d.one - (2 * d.h) • O.product d.eta d.uStar.

Equations

• NavierStokes.AxisContraction.angularLinearCoefficient O d = d.wStar + d.h • d.one - (2 * d.h) • (O.product d.eta) d.uStar

noncomputable def NavierStokes.AxisContraction.angularQuadraticCoefficient {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] (O : NaturalOperators V) (d : AxisData V) : V

Angular quadratic coefficient, given by O.product d.d d.normalizedGradient.

Equations

• NavierStokes.AxisContraction.angularQuadraticCoefficient O d = (O.product d.d) d.normalizedGradient

def NavierStokes.AxisContraction.averageCoefficient {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] (d : AxisData V) : V

Average coefficient, given by (2 * d.D) • d.eta.

Equations

• NavierStokes.AxisContraction.averageCoefficient d = (2 * d.D) • d.eta

def NavierStokes.AxisContraction.angularSlowCoefficient {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] (d : AxisData V) : V

Angular slow coefficient, given by (2 * d.h) • d.eta.

Equations

• NavierStokes.AxisContraction.angularSlowCoefficient d = (2 * d.h) • d.eta

noncomputable def NavierStokes.AxisContraction.axialLinearCoefficient {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] (O : NaturalOperators V) (d : AxisData V) : V

Axial linear coefficient, given by d.A • d.one - (4 * d.A) • O.product d.eta d.uStar + O.product d.d d.uStarEta.

Equations

• NavierStokes.AxisContraction.axialLinearCoefficient O d = d.A • d.one - (4 * d.A) • (O.product d.eta) d.uStar + (O.product d.d) d.uStarEta

def NavierStokes.AxisContraction.axialQuadraticCoefficient {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] (d : AxisData V) : V

Axial quadratic coefficient, given by (2 * d.A) • d.eta.

Equations

• NavierStokes.AxisContraction.axialQuadraticCoefficient d = (2 * d.A) • d.eta

noncomputable def NavierStokes.AxisContraction.naturalRemainder {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] (O : NaturalOperators V) (d : AxisData V) (S : V →L[ℝ] V) (t : ℝ) (a : V) (x : V × V) : V × V

The exact expanded, radially integrated nonlinear remainders. The first component also includes the bounded angular resolvent. Here t is Λ⁻¹ and a is φ*/C.

Equations

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

noncomputable def NavierStokes.AxisContraction.referencePair {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] (O : NaturalOperators V) (d : AxisData V) (S : V →L[ℝ] V) : V × V

The reference pair about which the nonlinear iteration is performed.

Equations

• NavierStokes.AxisContraction.referencePair O d S = (S d.one, -(1 / 2) • O.j1 ((O.product d.inverseL) d.zStar))

theorem NavierStokes.AxisContraction.angular_remainder_expansion (t h D η d U W H κ φ u bu buη φdot φη : ℝ) : (W + h - 2 * h * η * U) * φ + W * φdot + H * φη + d * κ * u * φ - t * ((2 * D * η * bu + 2 * h * η * u) * φ + d * buη * φ + 2 * D * η * bu * φdot + d * buη * φdot - d * u * φη) = (W - t * (2 * D * η * bu + d * buη) + h * (1 - 2 * η * (U + t * u)) + d * u * κ) * φ + (W - t * (2 * D * η * bu + d * buη)) * φdot + (H + t * d * u) * φη

Scalar check of the angular grouping used before applying the actual linear radial inverse. No derivative terms are omitted in the expansion.

theorem NavierStokes.AxisContraction.axial_remainder_expansion (t A D η d U Uη W H u bu buη udot uη P Pη Pdot : ℝ) : (A - 4 * A * η * U + d * Uη) * u + W * udot + H * uη - t * (2 * A * η * (u * u) + 2 * D * η * bu * udot + d * buη * udot - d * u * uη) + (-4 * A * η * P + d * Pη - 2 * η * Pdot) = A * (1 - 4 * η * U) * u - 2 * A * η * t * (u * u) + (W - t * (2 * D * η * bu + d * buη)) * udot + H * uη + d * Uη * u + t * d * u * uη - 4 * A * η * P + d * Pη - 2 * η * Pdot

Scalar check of the axial grouping, including the pressure terms.

noncomputable def NavierStokes.AxisContraction.controlledRemainder {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] (O : NaturalOperators V) (d : AxisData V) (S : V →L[ℝ] V) (R M : ℝ) (hR : 0 ≤ R) (hM : 0 ≤ M) (t : ℝ) (ht : |t| ≤ 1) (a : V) (ha : ‖a‖ ≤ M) : Controlled (V × V) (V × V) R

Explicit propagation of local bounds through every term in the actual integrated remainders. Its numerical fields do not depend on t or a, only on the uniform upper bound M for the norm of a.

Equations

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

@[simp]

theorem NavierStokes.AxisContraction.controlledRemainder_eval {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] (O : NaturalOperators V) (d : AxisData V) (S : V →L[ℝ] V) (R M : ℝ) (hR : 0 ≤ R) (hM : 0 ≤ M) (t : ℝ) (ht : |t| ≤ 1) (a : V) (ha : ‖a‖ ≤ M) (x : V × V) : (controlledRemainder O d S R M hR hM t ht a ha).eval x = naturalRemainder O d S t a x

noncomputable def NavierStokes.AxisContraction.remainderBound {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] (O : NaturalOperators V) (d : AxisData V) (S : V →L[ℝ] V) (R M : ℝ) (hR : 0 ≤ R) (hM : 0 ≤ M) : ℝ

An explicit expression in the fixed operator norms, coefficient norms, ball radius, and upper bound for the pressure amplitude.

Equations

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

noncomputable def NavierStokes.AxisContraction.remainderLip {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] (O : NaturalOperators V) (d : AxisData V) (S : V →L[ℝ] V) (R M : ℝ) (hR : 0 ≤ R) (hM : 0 ≤ M) : ℝ

Remainder lip, given by (controlledRemainder O d S R M hR hM 0 (by simp) 0 (by simpa using hM)).lip.

Equations

• NavierStokes.AxisContraction.remainderLip O d S R M hR hM = (NavierStokes.AxisContraction.controlledRemainder O d S R M hR hM 0 NavierStokes.AxisContraction.remainderBound._proof_1 0 ⋯).lip

theorem NavierStokes.AxisContraction.controlledRemainder_bound_eq {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] (O : NaturalOperators V) (d : AxisData V) (S : V →L[ℝ] V) (R M : ℝ) (hR : 0 ≤ R) (hM : 0 ≤ M) (t : ℝ) (ht : |t| ≤ 1) (a : V) (ha : ‖a‖ ≤ M) : (controlledRemainder O d S R M hR hM t ht a ha).bound = remainderBound O d S R M hR hM

theorem NavierStokes.AxisContraction.controlledRemainder_lip_eq {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] (O : NaturalOperators V) (d : AxisData V) (S : V →L[ℝ] V) (R M : ℝ) (hR : 0 ≤ R) (hM : 0 ≤ M) (t : ℝ) (ht : |t| ≤ 1) (a : V) (ha : ‖a‖ ≤ M) : (controlledRemainder O d S R M hR hM t ht a ha).lip = remainderLip O d S R M hR hM

theorem NavierStokes.AxisContraction.remainderBound_nonneg {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] (O : NaturalOperators V) (d : AxisData V) (S : V →L[ℝ] V) (R M : ℝ) (hR : 0 ≤ R) (hM : 0 ≤ M) : 0 ≤ remainderBound O d S R M hR hM

theorem NavierStokes.AxisContraction.remainderLip_nonneg {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] (O : NaturalOperators V) (d : AxisData V) (S : V →L[ℝ] V) (R M : ℝ) (hR : 0 ≤ R) (hM : 0 ≤ M) : 0 ≤ remainderLip O d S R M hR hM

theorem NavierStokes.AxisContraction.norm_naturalRemainder_le {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] (O : NaturalOperators V) (d : AxisData V) (S : V →L[ℝ] V) (R M : ℝ) (hR : 0 ≤ R) (hM : 0 ≤ M) (t : ℝ) (ht : |t| ≤ 1) (a : V) (ha : ‖a‖ ≤ M) (x : V × V) (hx : ‖x‖ ≤ R) : ‖naturalRemainder O d S t a x‖ ≤ remainderBound O d S R M hR hM

The actual remainder is bounded uniformly in both the small parameter and every normalized angular amplitude with norm at most M.

theorem NavierStokes.AxisContraction.naturalRemainder_sub_le {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] (O : NaturalOperators V) (d : AxisData V) (S : V →L[ℝ] V) (R M : ℝ) (hR : 0 ≤ R) (hM : 0 ≤ M) (t : ℝ) (ht : |t| ≤ 1) (a : V) (ha : ‖a‖ ≤ M) (x y : V × V) (hx : ‖x‖ ≤ R) (hy : ‖y‖ ≤ R) : ‖naturalRemainder O d S t a x - naturalRemainder O d S t a y‖ ≤ remainderLip O d S R M hR hM * ‖x - y‖

The local Lipschitz estimate is derived term by term from the actual polynomial operators, including the mixed and pressure terms.

noncomputable def NavierStokes.AxisContraction.contractionThreshold {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] (O : NaturalOperators V) (d : AxisData V) (S : V →L[ℝ] V) (x₀ : V × V) (M : ℝ) (hM : 0 ≤ M) : ℝ

A finite threshold depending only on fixed operator/coefficient data, the reference pair, and the uniform norm bound M. In particular it does not depend on the normalized amplitude a.

Equations

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

theorem NavierStokes.AxisContraction.contractionThreshold_pos {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] (O : NaturalOperators V) (d : AxisData V) (S : V →L[ℝ] V) (x₀ : V × V) (M : ℝ) (hM : 0 ≤ M) : 0 < contractionThreshold O d S x₀ M hM

theorem NavierStokes.AxisContraction.exists_unique_natural_fixedPoint {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] (O : NaturalOperators V) (d : AxisData V) (S : V →L[ℝ] V) (x₀ : V × V) (M : ℝ) (hM : 0 ≤ M) (Λ : ℝ) (hΛ : contractionThreshold O d S x₀ M hM ≤ Λ) (a : V) (ha : ‖a‖ ≤ M) : ∃ (x : V × V), ‖x - x₀‖ ≤ 1 ∧ x₀ + (1 / (2 * Λ)) • naturalRemainder O d S (1 / Λ) a x = x ∧ ‖x - x₀‖ ≤ remainderBound O d S (‖x₀‖ + 1) M ⋯ hM / (2 * Λ) ∧ ∀ (y : V × V), ‖y - x₀‖ ≤ 1 → x₀ + (1 / (2 * Λ)) • naturalRemainder O d S (1 / Λ) a y = y → y = x

Existence, uniqueness in the reference ball, and an explicit O(Λ⁻¹) norm error for the actual polynomial remainders. The two remainder estimates used here were proved above term by term.

theorem NavierStokes.AxisContraction.uniform_natural_fixedPoint {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] (O : NaturalOperators V) (d : AxisData V) (S : V →L[ℝ] V) (M : ℝ) (hM : 0 ≤ M) : ∃ (Λ₀ : ℝ), 0 < Λ₀ ∧ ∀ (Λ : ℝ), Λ₀ ≤ Λ → ∀ (a : V), ‖a‖ ≤ M → ∃ (x : V × V), ‖x - referencePair O d S‖ ≤ 1 ∧ referencePair O d S + (1 / (2 * Λ)) • naturalRemainder O d S (1 / Λ) a x = x ∧ ‖x - referencePair O d S‖ ≤ remainderBound O d S (‖referencePair O d S‖ + 1) M ⋯ hM / (2 * Λ) ∧ ∀ (y : V × V), ‖y - referencePair O d S‖ ≤ 1 → referencePair O d S + (1 / (2 * Λ)) • naturalRemainder O d S (1 / Λ) a y = y → y = x

The same threshold works for every admissible a = φ*/C; the normalization hypothesis is a norm bound on the actual coefficient input, not a hypothesis about the nonlinear map's Lipschitz constant.

theorem NavierStokes.AxisContraction.naturalRemainder_fst_resolvent {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] (O : NaturalOperators V) (d : AxisData V) (S : V →L[ℝ] V) (t : ℝ) (a : V) (x : V × V) : (naturalRemainder O d S t a x).1 = S (naturalRemainder O d (ContinuousLinearMap.id ℝ V) t a x).1

theorem NavierStokes.AxisContraction.naturalRemainder_snd_resolvent {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] (O : NaturalOperators V) (d : AxisData V) (S : V →L[ℝ] V) (t : ℝ) (a : V) (x : V × V) : (naturalRemainder O d S t a x).2 = (naturalRemainder O d (ContinuousLinearMap.id ℝ V) t a x).2

theorem NavierStokes.AxisContraction.fixedPoint_integrated_equations {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] (O : NaturalOperators V) (d : AxisData V) (S Q : V →L[ℝ] V) (hS : ∀ (y : V), S y + Q (S y) = y) (t s : ℝ) (a : V) (x : V × V) (hfixed : referencePair O d S + s • naturalRemainder O d S t a x = x) : x.1 + Q x.1 = d.one + s • (naturalRemainder O d (ContinuousLinearMap.id ℝ V) t a x).1 ∧ x.2 = -(1 / 2) • O.j1 ((O.product d.inverseL) d.zStar) + s • (naturalRemainder O d (ContinuousLinearMap.id ℝ V) t a x).2

Undoing the actual angular resolvent turns the fixed point into the two integrated natural equations. The only extra hypothesis is the resolvent identity, independently proved in AxisResolvent.

theorem NavierStokes.AxisContraction.integrated_equations_fixedPoint {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] (O : NaturalOperators V) (d : AxisData V) (S Q : V →L[ℝ] V) (hS : ∀ (y : V), S (y + Q y) = y) (t s : ℝ) (a : V) (x : V × V) (hφ : x.1 + Q x.1 = d.one + s • (naturalRemainder O d (ContinuousLinearMap.id ℝ V) t a x).1) (hu : x.2 = -(1 / 2) • O.j1 ((O.product d.inverseL) d.zStar) + s • (naturalRemainder O d (ContinuousLinearMap.id ℝ V) t a x).2) : referencePair O d S + s • naturalRemainder O d S t a x = x

With the left resolvent identity, the two integrated equations also imply the nonlinear fixed-point equation.

theorem NavierStokes.AxisContraction.axis_angular_jet_error (I : AxisCoefficientSpace.Window) (ε : ℝ) (x x₀ : ↥(AxisCoefficientSpace.AxisSpace I ε) × ↥(AxisCoefficientSpace.AxisSpace I ε)) (B : ℝ) (hB : ‖x - x₀‖ ≤ B) (n m : ℕ) (η : ℝ) : |AxisCoefficientSpace.jet I (AxisWeightEstimates.weight ε) (↑x.1) n m η - AxisCoefficientSpace.jet I (AxisWeightEstimates.weight ε) (↑x₀.1) n m η| ≤ |AxisWeightEstimates.weight ε n m| * B

A single coefficient-space norm error controls every angular parameter jet uniformly on the full real parameter interval.

theorem NavierStokes.AxisContraction.axis_axial_jet_error (I : AxisCoefficientSpace.Window) (ε : ℝ) (x x₀ : ↥(AxisCoefficientSpace.AxisSpace I ε) × ↥(AxisCoefficientSpace.AxisSpace I ε)) (B : ℝ) (hB : ‖x - x₀‖ ≤ B) (n m : ℕ) (η : ℝ) : |AxisCoefficientSpace.jet I (AxisWeightEstimates.weight ε) (↑x.2) n m η - AxisCoefficientSpace.jet I (AxisWeightEstimates.weight ε) (↑x₀.2) n m η| ≤ |AxisWeightEstimates.weight ε n m| * B

The same uniform control for every axial parameter jet.

theorem NavierStokes.AxisContraction.evaluated_mixed_error (I : AxisCoefficientSpace.Window) {ε R : ℝ} (hε : 0 < ε) (hR : 1 ≤ R) (hR20 : R < 20) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (K : ℝ) (hK : ‖A - B‖ ≤ K) (k m : ℕ) {Y η : ℝ} (hY : |Y| ≤ R) (hη : η ∈ Set.Ioo I.left I.right) : ‖iteratedDeriv m (fun (z : ℝ) => iteratedDeriv k (fun (y : ℝ) => AxisEvaluation.profile I ε A (y, z)) Y) η - iteratedDeriv m (fun (z : ℝ) => iteratedDeriv k (fun (y : ℝ) => AxisEvaluation.profile I ε B (y, z)) Y) η‖ ≤ AxisEvaluation.jetBound ε R k m * K

The coefficient fixed-point error controls actual mixed derivatives of the evaluated functions, uniformly on every smaller radial interval.

noncomputable def NavierStokes.AxisContraction.coefficientOperators (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) : NaturalOperators ↥(AxisCoefficientSpace.AxisSpace I ε)

Concrete instantiation by the genuine coefficient product, radial averages/inverses, and derivative composites constructed in AxisOperators.

Equations

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

theorem NavierStokes.AxisContraction.coefficient_fixedPoint (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (d : AxisData ↥(AxisCoefficientSpace.AxisSpace I ε)) (S : ↥(AxisCoefficientSpace.AxisSpace I ε) →L[ℝ] ↥(AxisCoefficientSpace.AxisSpace I ε)) (M : ℝ) (hM : 0 ≤ M) : let O := coefficientOperators I hε; ∃ (Λ₀ : ℝ), 0 < Λ₀ ∧ ∀ (Λ : ℝ), Λ₀ ≤ Λ → ∀ (a : ↥(AxisCoefficientSpace.AxisSpace I ε)), ‖a‖ ≤ M → ∃ (x : ↥(AxisCoefficientSpace.AxisSpace I ε) × ↥(AxisCoefficientSpace.AxisSpace I ε)), ‖x - referencePair O d S‖ ≤ 1 ∧ referencePair O d S + (1 / (2 * Λ)) • naturalRemainder O d S (1 / Λ) a x = x ∧ ‖x - referencePair O d S‖ ≤ remainderBound O d S (‖referencePair O d S‖ + 1) M ⋯ hM / (2 * Λ) ∧ ∀ (y : ↥(AxisCoefficientSpace.AxisSpace I ε) × ↥(AxisCoefficientSpace.AxisSpace I ε)), ‖y - referencePair O d S‖ ≤ 1 → referencePair O d S + (1 / (2 * Λ)) • naturalRemainder O d S (1 / Λ) a y = y → y = x

The nonlinear map on the actual complete smooth coefficient space has a single threshold valid for all normalized angular data in a fixed norm ball. No remainder bound is supplied as a hypothesis.

theorem NavierStokes.AxisContraction.natural_axis_profiles (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (d : AxisData ↥(AxisCoefficientSpace.AxisSpace I ε)) (M : ℝ) (hM : 0 ≤ M) : let O := coefficientOperators I hε; let S := AxisResolvent.naturalResolvent I hε χ; have Q := AxisResolvent.naturalOperator I hε χ; let x₀ := referencePair O d S; ∃ (Λ₀ : ℝ), 0 < Λ₀ ∧ ∀ (Λ : ℝ), Λ₀ ≤ Λ → ∀ (a : ↥(AxisCoefficientSpace.AxisSpace I ε)), ‖a‖ ≤ M → ∃ (x : ↥(AxisCoefficientSpace.AxisSpace I ε) × ↥(AxisCoefficientSpace.AxisSpace I ε)), ‖x - x₀‖ ≤ 1 ∧ ‖x - x₀‖ ≤ remainderBound O d S (‖x₀‖ + 1) M ⋯ hM / (2 * Λ) ∧ x.1 + Q x.1 = d.one + (1 / (2 * Λ)) • (naturalRemainder O d (ContinuousLinearMap.id ℝ ↥(AxisCoefficientSpace.AxisSpace I ε)) (1 / Λ) a x).1 ∧ x.2 = -(1 / 2) • O.j1 ((O.product d.inverseL) d.zStar) + (1 / (2 * Λ)) • (naturalRemainder O d (ContinuousLinearMap.id ℝ ↥(AxisCoefficientSpace.AxisSpace I ε)) (1 / Λ) a x).2 ∧ ContDiffOn ℝ (↑⊤) (AxisEvaluation.profile I ε x.1) (AxisEvaluation.strip I 20) ∧ ContDiffOn ℝ (↑⊤) (AxisEvaluation.profile I ε x.2) (AxisEvaluation.strip I 20)

Existence of actual smooth coefficient profiles for the natural integrated system, with the constructed angular resolvent and uniform large-Λ estimate. The initial analytic coefficient data remain explicit.

Actual profile equations for the coefficient operators

The identities here combine the convergent, smooth evaluation of AxisSpace with the exact compatible coefficient operators of AxisOperators.

theorem NavierStokes.AxisEvaluationAlgebra.powerSeries_mul {f g : ℕ → ℝ} {Y : ℝ} (hf : Summable fun (n : ℕ) => ‖Y ^ n * f n‖) (hg : Summable fun (n : ℕ) => ‖Y ^ n * g n‖) : (∑' (n : ℕ), Y ^ n * f n) * ∑' (n : ℕ), Y ^ n * g n = ∑' (n : ℕ), Y ^ n * ∑ ij ∈ Finset.antidiagonal n, f ij.1 * g ij.2

theorem NavierStokes.AxisEvaluationAlgebra.profile_series_norm_summable (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {Y η : ℝ} (hY : |Y| < 20) : Summable fun (n : ℕ) => ‖Y ^ n * AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) A n η‖

theorem NavierStokes.AxisEvaluationAlgebra.profile_product (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) {Y η : ℝ} (hY : |Y| < 20) (hη : η ∈ I.interval) : AxisEvaluation.profile I ε (((AxisOperators.product I hε) A) B) (Y, η) = AxisEvaluation.profile I ε A (Y, η) * AxisEvaluation.profile I ε B (Y, η)

Multiplication in the coefficient space evaluates to pointwise multiplication.

theorem NavierStokes.AxisEvaluationAlgebra.profile_axis (I : AxisCoefficientSpace.Window) (ε : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (η : ℝ) : AxisEvaluation.profile I ε A (0, η) = AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) A 0 η

theorem NavierStokes.AxisEvaluationAlgebra.profile_deriv_Y (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {Y η : ℝ} (hY : Y ∈ Set.Ioo (-20) 20) (hη : η ∈ Set.Ioo I.left I.right) : deriv (fun (y : ℝ) => AxisEvaluation.profile I ε A (y, η)) Y = AxisEvaluation.mixedSeries I ε A 1 0 (Y, η)

theorem NavierStokes.AxisEvaluationAlgebra.profile_deriv_eta (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {Y η : ℝ} (hY : Y ∈ Set.Ioo (-20) 20) (hη : η ∈ Set.Ioo I.left I.right) : deriv (fun (x : ℝ) => AxisEvaluation.profile I ε A (Y, x)) η = AxisEvaluation.mixedSeries I ε A 0 1 (Y, η)

theorem NavierStokes.AxisEvaluationAlgebra.profile_iteratedDeriv_Y (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k : ℕ) {Y η : ℝ} (hY : Y ∈ Set.Ioo (-20) 20) (hη : η ∈ Set.Ioo I.left I.right) : iteratedDeriv k (fun (y : ℝ) => AxisEvaluation.profile I ε A (y, η)) Y = AxisEvaluation.mixedSeries I ε A k 0 (Y, η)

noncomputable def NavierStokes.AxisEvaluationAlgebra.radialValue (I : AxisCoefficientSpace.Window) (ε : ℝ) (r : ℕ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (p : ℝ × ℝ) : ℝ

Radial value, given by p.1 * mixedSeries I ε A 2 0 p + (r : ℝ) * mixedSeries I ε A 1 0 p.

Equations

• NavierStokes.AxisEvaluationAlgebra.radialValue I ε r A p = p.1 * NavierStokes.AxisEvaluation.mixedSeries I ε A 2 0 p + ↑r * NavierStokes.AxisEvaluation.mixedSeries I ε A 1 0 p

theorem NavierStokes.AxisEvaluationAlgebra.radialValue_eq_derivatives (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {Y η : ℝ} (hY : Y ∈ Set.Ioo (-20) 20) (hη : η ∈ Set.Ioo I.left I.right) : radialValue I ε r A (Y, η) = Y * iteratedDeriv 2 (fun (y : ℝ) => AxisEvaluation.profile I ε A (y, η)) Y + ↑r * deriv (fun (y : ℝ) => AxisEvaluation.profile I ε A (y, η)) Y

theorem NavierStokes.AxisEvaluationAlgebra.polynomialJet_radial (r n : ℕ) (Y : ℝ) : Y * AxisEvaluation.polynomialJet (n + 1) 2 Y + ↑r * AxisEvaluation.polynomialJet (n + 1) 1 Y = AxisWeightEstimates.radialDivisor r n * Y ^ n

theorem NavierStokes.AxisEvaluationAlgebra.radialValue_series (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {Y η : ℝ} (hY : |Y| < 20) : radialValue I ε r A (Y, η) = ∑' (n : ℕ), AxisWeightEstimates.radialDivisor r n * Y ^ n * AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) A (n + 1) η

Coefficient formula for the actual regular radial differential operator.

theorem NavierStokes.AxisEvaluationAlgebra.regularInverse_equation (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {Y η : ℝ} (hY : |Y| < 20) (hη : η ∈ I.interval) : radialValue I ε r ((AxisOperators.regularInverse I hε r hr) A) (Y, η) = AxisEvaluation.profile I ε A (Y, η)

The regular inverse is a genuine right inverse on evaluated profiles.

theorem NavierStokes.AxisEvaluationAlgebra.regularInverse_axis_zero (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {η : ℝ} (hη : η ∈ I.interval) : AxisEvaluation.profile I ε ((AxisOperators.regularInverse I hε r hr) A) (0, η) = 0

theorem NavierStokes.AxisEvaluationAlgebra.derivativeSeries (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {Y η : ℝ} (hY : |Y| < 20) : AxisEvaluation.mixedSeries I ε A 1 0 (Y, η) = ∑' (n : ℕ), (↑n + 1) * Y ^ n * AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) A (n + 1) η

theorem NavierStokes.AxisEvaluationAlgebra.jet_average_eval (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) {η : ℝ} (hη : η ∈ I.interval) : AxisOperators.inputJet I ε ((AxisOperators.average I hε) A) n m η = AxisOperators.inputJet I ε A n m η / (↑n + 1)

theorem NavierStokes.AxisEvaluationAlgebra.jet_primitive_eval (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) {η : ℝ} (hη : η ∈ I.interval) : AxisOperators.inputJet I ε ((AxisOperators.primitive I hε) A) n m η = AxisOperators.primitiveScale n * AxisOperators.inputJet I ε A n.pred m η

theorem NavierStokes.AxisEvaluationAlgebra.jet_parameterPrimitive_eval (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) {η : ℝ} (hη : η ∈ I.interval) : AxisOperators.inputJet I ε ((AxisOperators.parameterPrimitive I hε) A) n m η = AxisOperators.primitiveScale n * AxisOperators.inputJet I ε A n.pred (1 + m) η

theorem NavierStokes.AxisEvaluationAlgebra.jet_mulY_eval (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) {η : ℝ} (hη : η ∈ I.interval) : AxisOperators.inputJet I ε ((AxisOperators.mulY I hε) A) n m η = AxisOperators.multiplyYScale n * AxisOperators.inputJet I ε A n.pred m η

theorem NavierStokes.AxisEvaluationAlgebra.primitive_Y_value (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {Y η : ℝ} (hY : |Y| < 20) (hη : η ∈ I.interval) : AxisEvaluation.mixedSeries I ε ((AxisOperators.primitive I hε) A) 1 0 (Y, η) = AxisEvaluation.profile I ε A (Y, η)

theorem NavierStokes.AxisEvaluationAlgebra.primitive_hasDerivAt (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {Y η : ℝ} (hY : Y ∈ Set.Ioo (-20) 20) (hη : η ∈ Set.Ioo I.left I.right) : HasDerivAt (fun (y : ℝ) => AxisEvaluation.profile I ε ((AxisOperators.primitive I hε) A) (y, η)) (AxisEvaluation.profile I ε A (Y, η)) Y

theorem NavierStokes.AxisEvaluationAlgebra.primitive_axis_zero (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {η : ℝ} (hη : η ∈ I.interval) : AxisEvaluation.profile I ε ((AxisOperators.primitive I hε) A) (0, η) = 0

theorem NavierStokes.AxisEvaluationAlgebra.profile_mulY (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {Y η : ℝ} (hY : |Y| < 20) (hη : η ∈ I.interval) : AxisEvaluation.profile I ε ((AxisOperators.mulY I hε) A) (Y, η) = Y * AxisEvaluation.profile I ε A (Y, η)

theorem NavierStokes.AxisEvaluationAlgebra.primitive_eq_mulY_average (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) : (AxisOperators.primitive I hε) A = (AxisOperators.mulY I hε) ((AxisOperators.average I hε) A)

theorem NavierStokes.AxisEvaluationAlgebra.average_times_Y (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {Y η : ℝ} (hY : |Y| < 20) (hη : η ∈ I.interval) : Y * AxisEvaluation.profile I ε ((AxisOperators.average I hε) A) (Y, η) = AxisEvaluation.profile I ε ((AxisOperators.primitive I hε) A) (Y, η)

theorem NavierStokes.AxisEvaluationAlgebra.parameterSeries (I : AxisCoefficientSpace.Window) (ε : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (m : ℕ) (Y η : ℝ) : AxisEvaluation.mixedSeries I ε A 0 m (Y, η) = ∑' (n : ℕ), Y ^ n * AxisOperators.inputJet I ε A n m η

theorem NavierStokes.AxisEvaluationAlgebra.parameterSeries_norm_summable (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (m : ℕ) {Y η : ℝ} (hY : |Y| < 20) : Summable fun (n : ℕ) => ‖Y ^ n * AxisOperators.inputJet I ε A n m η‖

theorem NavierStokes.AxisEvaluationAlgebra.polynomialJet_dot (n : ℕ) (Y : ℝ) : Y * AxisEvaluation.polynomialJet n 1 Y = ↑n * Y ^ n

theorem NavierStokes.AxisEvaluationAlgebra.dotSeries (I : AxisCoefficientSpace.Window) (ε : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (Y η : ℝ) : Y * AxisEvaluation.mixedSeries I ε A 1 0 (Y, η) = ∑' (n : ℕ), Y ^ n * (↑n * AxisOperators.inputJet I ε A n 0 η)

theorem NavierStokes.AxisEvaluationAlgebra.dotSeries_norm_summable (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {Y η : ℝ} (hY : |Y| < 20) : Summable fun (n : ℕ) => ‖Y ^ n * (↑n * AxisOperators.inputJet I ε A n 0 η)‖

theorem NavierStokes.AxisEvaluationAlgebra.radialValue_of_convolution (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (C : ↥(AxisCoefficientSpace.AxisSpace I ε)) (f g : ℕ → ℝ) {Y η : ℝ} (hY : |Y| < 20) (hf : Summable fun (n : ℕ) => ‖Y ^ n * f n‖) (hg : Summable fun (n : ℕ) => ‖Y ^ n * g n‖) (hC : ∀ (n : ℕ), AxisWeightEstimates.radialDivisor r n * AxisOperators.inputJet I ε C (n + 1) 0 η = ∑ ij ∈ Finset.antidiagonal n, f ij.1 * g ij.2) : radialValue I ε r C (Y, η) = (∑' (n : ℕ), Y ^ n * f n) * ∑' (n : ℕ), Y ^ n * g n

theorem NavierStokes.AxisEvaluationAlgebra.differentialFamily_cancel (I : AxisCoefficientSpace.Window) (ε : ℝ) (r p : ℕ) (hr : 1 ≤ r) (d : ℕ → ℝ) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n : ℕ) (η : ℝ) : AxisWeightEstimates.radialDivisor r n * AxisOperators.differentialFamily I ε r p d A B (n + 1) 0 η = ∑ ij ∈ Finset.antidiagonal n, AxisOperators.inputJet I ε A ij.1 p η * (d ij.2 * AxisOperators.inputJet I ε B ij.2 0 η)

theorem NavierStokes.AxisEvaluationAlgebra.inverseMixed_equation (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) {Y η : ℝ} (hY : |Y| < 20) (hη : η ∈ I.interval) : radialValue I ε r (((AxisOperators.inverseMixed I hε r hr) A) B) (Y, η) = AxisEvaluation.mixedSeries I ε A 0 1 (Y, η) * (Y * AxisEvaluation.mixedSeries I ε B 1 0 (Y, η))

The parameter derivative is on the first factor and the radial dot is on the second factor, as required by the manuscript's mixed estimate.

theorem NavierStokes.AxisEvaluationAlgebra.inverseParamProduct_equation (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) {Y η : ℝ} (hY : |Y| < 20) (hη : η ∈ I.interval) : radialValue I ε r (((AxisOperators.inverseParamProduct I hε r hr) A) B) (Y, η) = AxisEvaluation.mixedSeries I ε A 0 1 (Y, η) * AxisEvaluation.profile I ε B (Y, η)

theorem NavierStokes.AxisEvaluationAlgebra.inverseDotProduct_equation (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) {Y η : ℝ} (hY : |Y| < 20) (hη : η ∈ I.interval) : radialValue I ε r (((AxisOperators.inverseDotProduct I hε r hr) A) B) (Y, η) = AxisEvaluation.profile I ε A (Y, η) * (Y * AxisEvaluation.mixedSeries I ε B 1 0 (Y, η))

theorem NavierStokes.AxisEvaluationAlgebra.inverseMixed_axis_zero (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) {η : ℝ} (hη : η ∈ I.interval) : AxisEvaluation.profile I ε (((AxisOperators.inverseMixed I hε r hr) A) B) (0, η) = 0

theorem NavierStokes.AxisEvaluationAlgebra.inverseParamProduct_axis_zero (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) {η : ℝ} (hη : η ∈ I.interval) : AxisEvaluation.profile I ε (((AxisOperators.inverseParamProduct I hε r hr) A) B) (0, η) = 0

theorem NavierStokes.AxisEvaluationAlgebra.inverseDotProduct_axis_zero (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) {η : ℝ} (hη : η ∈ I.interval) : AxisEvaluation.profile I ε (((AxisOperators.inverseDotProduct I hε r hr) A) B) (0, η) = 0

theorem NavierStokes.AxisEvaluationAlgebra.parameterPrimitive_eta_value (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (Y : ℝ) {η : ℝ} (hη : η ∈ I.interval) : AxisEvaluation.profile I ε ((AxisOperators.parameterPrimitive I hε) A) (Y, η) = AxisEvaluation.mixedSeries I ε ((AxisOperators.primitive I hε) A) 0 1 (Y, η)

theorem NavierStokes.AxisEvaluationAlgebra.parameterPrimitive_eq_deriv_eta (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {Y η : ℝ} (hY : Y ∈ Set.Ioo (-20) 20) (hη : η ∈ Set.Ioo I.left I.right) : AxisEvaluation.profile I ε ((AxisOperators.parameterPrimitive I hε) A) (Y, η) = deriv (fun (x : ℝ) => AxisEvaluation.profile I ε ((AxisOperators.primitive I hε) A) (Y, x)) η

The pressure parameter primitive is the actual parameter derivative of the radial primitive.

theorem NavierStokes.AxisEvaluationAlgebra.parameterPrimitive_Y_value (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {Y η : ℝ} (hY : |Y| < 20) (hη : η ∈ I.interval) : AxisEvaluation.mixedSeries I ε ((AxisOperators.parameterPrimitive I hε) A) 1 0 (Y, η) = AxisEvaluation.mixedSeries I ε A 0 1 (Y, η)

theorem NavierStokes.AxisEvaluationAlgebra.parameterPrimitive_hasDerivAt (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {Y η : ℝ} (hY : Y ∈ Set.Ioo (-20) 20) (hη : η ∈ Set.Ioo I.left I.right) : HasDerivAt (fun (y : ℝ) => AxisEvaluation.profile I ε ((AxisOperators.parameterPrimitive I hε) A) (y, η)) (deriv (fun (x : ℝ) => AxisEvaluation.profile I ε A (Y, x)) η) Y

theorem NavierStokes.AxisEvaluationAlgebra.parameterPrimitive_axis_zero (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {η : ℝ} (hη : η ∈ I.interval) : AxisEvaluation.profile I ε ((AxisOperators.parameterPrimitive I hε) A) (0, η) = 0

theorem NavierStokes.AxisEvaluationAlgebra.radial_segment_mem {Y y : ℝ} (hY : Y ∈ Set.Ioo (-20) 20) (hy : y ∈ Set.uIcc 0 Y) : y ∈ Set.Ioo (-20) 20

theorem NavierStokes.AxisEvaluationAlgebra.primitive_integral (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {Y η : ℝ} (hY : Y ∈ Set.Ioo (-20) 20) (hη : η ∈ Set.Ioo I.left I.right) : AxisEvaluation.profile I ε ((AxisOperators.primitive I hε) A) (Y, η) = ∫ (y : ℝ) in 0..Y, AxisEvaluation.profile I ε A (y, η)

The coefficient primitive equals the ordinary oriented integral.

theorem NavierStokes.AxisEvaluationAlgebra.average_integral (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {Y η : ℝ} (hY : Y ∈ Set.Ioo (-20) 20) (hη : η ∈ Set.Ioo I.left I.right) : Y * AxisEvaluation.profile I ε ((AxisOperators.average I hε) A) (Y, η) = ∫ (y : ℝ) in 0..Y, AxisEvaluation.profile I ε A (y, η)

theorem NavierStokes.AxisEvaluationAlgebra.regularInverse_actual_equation (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {Y η : ℝ} (hY : Y ∈ Set.Ioo (-20) 20) (hη : η ∈ Set.Ioo I.left I.right) : Y * iteratedDeriv 2 (fun (y : ℝ) => AxisEvaluation.profile I ε ((AxisOperators.regularInverse I hε r hr) A) (y, η)) Y + ↑r * deriv (fun (y : ℝ) => AxisEvaluation.profile I ε ((AxisOperators.regularInverse I hε r hr) A) (y, η)) Y = AxisEvaluation.profile I ε A (Y, η)

theorem NavierStokes.AxisEvaluationAlgebra.inverseMixed_actual_equation (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) {Y η : ℝ} (hY : Y ∈ Set.Ioo (-20) 20) (hη : η ∈ Set.Ioo I.left I.right) : Y * iteratedDeriv 2 (fun (y : ℝ) => AxisEvaluation.profile I ε (((AxisOperators.inverseMixed I hε r hr) A) B) (y, η)) Y + ↑r * deriv (fun (y : ℝ) => AxisEvaluation.profile I ε (((AxisOperators.inverseMixed I hε r hr) A) B) (y, η)) Y = deriv (fun (x : ℝ) => AxisEvaluation.profile I ε A (Y, x)) η * (Y * deriv (fun (y : ℝ) => AxisEvaluation.profile I ε B (y, η)) Y)

theorem NavierStokes.AxisEvaluationAlgebra.average_axis (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {η : ℝ} (hη : η ∈ I.interval) : AxisEvaluation.profile I ε ((AxisOperators.average I hε) A) (0, η) = AxisEvaluation.profile I ε A (0, η)

theorem NavierStokes.AxisEvaluationAlgebra.average_equation (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {Y η : ℝ} (hY : |Y| < 20) (hη : η ∈ I.interval) : AxisEvaluation.profile I ε ((AxisOperators.average I hε) A) (Y, η) + Y * AxisEvaluation.mixedSeries I ε ((AxisOperators.average I hε) A) 1 0 (Y, η) = AxisEvaluation.profile I ε A (Y, η)

@[instance_reducible]

noncomputable def NavierStokes.NaturalAxisBridge.instNaturalAxisBridge1 (I : AxisCoefficientSpace.Window) (ε : ℝ) : NormedAddCommGroup ↥(AxisCoefficientSpace.AxisSpace I ε)

Cache the standard NormedAddCommGroup (AxisCoefficientSpace.AxisSpace I ε) instance to shorten typeclass synthesis.

Equations

• NavierStokes.NaturalAxisBridge.instNaturalAxisBridge1 I ε = inferInstance

@[instance_reducible]

noncomputable def NavierStokes.NaturalAxisBridge.instNaturalAxisBridge2 (I : AxisCoefficientSpace.Window) (ε : ℝ) : NormedSpace ℝ ↥(AxisCoefficientSpace.AxisSpace I ε)

Cache the standard NormedSpace ℝ (AxisCoefficientSpace.AxisSpace I ε) instance to shorten typeclass synthesis.

Equations

• NavierStokes.NaturalAxisBridge.instNaturalAxisBridge2 I ε = inferInstance

noncomputable def NavierStokes.NaturalAxisBridge.partialY (F : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Ordinary radial partial derivative of an actual function.

Equations

• NavierStokes.NaturalAxisBridge.partialY F p = deriv (fun (Y : ℝ) => F (Y, p.2)) p.1

noncomputable def NavierStokes.NaturalAxisBridge.partialEta (F : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Ordinary parameter partial derivative of an actual function.

Equations

• NavierStokes.NaturalAxisBridge.partialEta F p = deriv (fun (η : ℝ) => F (p.1, η)) p.2

noncomputable def NavierStokes.NaturalAxisBridge.mixedDerivative (k m : ℕ) (F : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Actual mixed derivative, with the order used by the manuscript's jet bounds.

Equations

• NavierStokes.NaturalAxisBridge.mixedDerivative k m F p = iteratedDeriv m (fun (η : ℝ) => iteratedDeriv k (fun (Y : ℝ) => F (Y, η)) p.1) p.2

noncomputable def NavierStokes.NaturalAxisBridge.radialDifferential (r : ℕ) (F : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

The singular radial differential expression, evaluated without division by Y.

Equations

• NavierStokes.NaturalAxisBridge.radialDifferential r F p = p.1 * iteratedDeriv 2 (fun (Y : ℝ) => F (Y, p.2)) p.1 + ↑r * NavierStokes.NaturalAxisBridge.partialY F p

noncomputable def NavierStokes.NaturalAxisBridge.radialEvaluation (I : AxisCoefficientSpace.Window) (ε : ℝ) (r : ℕ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (p : ℝ × ℝ) : ℝ

The same expression in terms of the rigorously differentiated sums.

Equations

• NavierStokes.NaturalAxisBridge.radialEvaluation I ε r A p = p.1 * NavierStokes.AxisEvaluation.mixedSeries I ε A 2 0 p + ↑r * NavierStokes.AxisEvaluation.mixedSeries I ε A 1 0 p

theorem NavierStokes.NaturalAxisBridge.partialY_profile (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {p : ℝ × ℝ} (hp : p ∈ AxisEvaluation.strip I 20) : partialY (AxisEvaluation.profile I ε A) p = AxisEvaluation.mixedSeries I ε A 1 0 p

theorem NavierStokes.NaturalAxisBridge.partialEta_profile (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {p : ℝ × ℝ} (hp : p ∈ AxisEvaluation.strip I 20) : partialEta (AxisEvaluation.profile I ε A) p = AxisEvaluation.mixedSeries I ε A 0 1 p

theorem NavierStokes.NaturalAxisBridge.mixedDerivative_profile (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m : ℕ) {p : ℝ × ℝ} (hp : p ∈ AxisEvaluation.strip I 20) : mixedDerivative k m (AxisEvaluation.profile I ε A) p = AxisEvaluation.mixedSeries I ε A k m p

theorem NavierStokes.NaturalAxisBridge.radialEvaluation_eq (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {p : ℝ × ℝ} (hp : p ∈ AxisEvaluation.strip I 20) : radialEvaluation I ε r A p = radialDifferential r (AxisEvaluation.profile I ε A) p

theorem NavierStokes.NaturalAxisBridge.profile_add (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) {p : ℝ × ℝ} (hp : |p.1| < 20) : AxisEvaluation.profile I ε (A + B) p = AxisEvaluation.profile I ε A p + AxisEvaluation.profile I ε B p

theorem NavierStokes.NaturalAxisBridge.profile_smul (I : AxisCoefficientSpace.Window) (ε c : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (p : ℝ × ℝ) : AxisEvaluation.profile I ε (c • A) p = c * AxisEvaluation.profile I ε A p

theorem NavierStokes.NaturalAxisBridge.profile_sub (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) {p : ℝ × ℝ} (hp : |p.1| < 20) : AxisEvaluation.profile I ε (A - B) p = AxisEvaluation.profile I ε A p - AxisEvaluation.profile I ε B p

theorem NavierStokes.NaturalAxisBridge.profile_zero (I : AxisCoefficientSpace.Window) (ε : ℝ) (p : ℝ × ℝ) : AxisEvaluation.profile I ε 0 p = 0

theorem NavierStokes.NaturalAxisBridge.radialEvaluation_add (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) {p : ℝ × ℝ} (hp : |p.1| < 20) : radialEvaluation I ε r (A + B) p = radialEvaluation I ε r A p + radialEvaluation I ε r B p

theorem NavierStokes.NaturalAxisBridge.radialEvaluation_sub (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) {p : ℝ × ℝ} (hp : |p.1| < 20) : radialEvaluation I ε r (A - B) p = radialEvaluation I ε r A p - radialEvaluation I ε r B p

theorem NavierStokes.NaturalAxisBridge.radialEvaluation_smul (I : AxisCoefficientSpace.Window) (ε c : ℝ) (r : ℕ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (p : ℝ × ℝ) : radialEvaluation I ε r (c • A) p = c * radialEvaluation I ε r A p

def NavierStokes.NaturalAxisBridge.RadiallyConstant (I : AxisCoefficientSpace.Window) (ε : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) : Prop

Fixed axis data have radial degree zero; parameter dependence remains unrestricted.

Equations

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

theorem NavierStokes.NaturalAxisBridge.profile_radiallyConstant (I : AxisCoefficientSpace.Window) (ε : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (hA : RadiallyConstant I ε A) (Y : ℝ) {η : ℝ} (hη : η ∈ I.interval) : AxisEvaluation.profile I ε A (Y, η) = AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) A 0 η

theorem NavierStokes.NaturalAxisBridge.radialEvaluation_constant (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (hA : RadiallyConstant I ε A) {p : ℝ × ℝ} (hp : p ∈ AxisEvaluation.strip I 20) : radialEvaluation I ε r A p = 0

theorem NavierStokes.NaturalAxisBridge.coefficient_product_constant (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (hA : RadiallyConstant I ε A) (n : ℕ) {η : ℝ} (hη : η ∈ I.interval) : AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) (((AxisOperators.product I hε) A) B) n η = AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) A 0 η * AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) B n η

theorem NavierStokes.NaturalAxisBridge.radialEvaluation_product_constant (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (hA : RadiallyConstant I ε A) {p : ℝ × ℝ} (hp : p ∈ AxisEvaluation.strip I 20) : radialEvaluation I ε r (((AxisOperators.product I hε) A) B) p = AxisEvaluation.profile I ε A p * radialEvaluation I ε r B p

A fixed parameter multiplier commutes with the radial differential expression.

theorem NavierStokes.NaturalAxisBridge.profile_neg (I : AxisCoefficientSpace.Window) (ε : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (p : ℝ × ℝ) : AxisEvaluation.profile I ε (-A) p = -AxisEvaluation.profile I ε A p

theorem NavierStokes.NaturalAxisBridge.radialEvaluation_regularInverse (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {p : ℝ × ℝ} (hp : p ∈ AxisEvaluation.strip I 20) : radialEvaluation I ε r ((AxisOperators.regularInverse I hε r hr) A) p = AxisEvaluation.profile I ε A p

theorem NavierStokes.NaturalAxisBridge.radialEvaluation_param (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) {p : ℝ × ℝ} (hp : p ∈ AxisEvaluation.strip I 20) : radialEvaluation I ε r (((AxisOperators.inverseParamProduct I hε r hr) A) B) p = partialEta (AxisEvaluation.profile I ε A) p * AxisEvaluation.profile I ε B p

theorem NavierStokes.NaturalAxisBridge.radialEvaluation_dot (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) {p : ℝ × ℝ} (hp : p ∈ AxisEvaluation.strip I 20) : radialEvaluation I ε r (((AxisOperators.inverseDotProduct I hε r hr) A) B) p = AxisEvaluation.profile I ε A p * (p.1 * partialY (AxisEvaluation.profile I ε B) p)

theorem NavierStokes.NaturalAxisBridge.radialEvaluation_mixed (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (r : ℕ) (hr : 1 ≤ r) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) {p : ℝ × ℝ} (hp : p ∈ AxisEvaluation.strip I 20) : radialEvaluation I ε r (((AxisOperators.inverseMixed I hε r hr) A) B) p = partialEta (AxisEvaluation.profile I ε A) p * (p.1 * partialY (AxisEvaluation.profile I ε B) p)

structure NavierStokes.NaturalAxisBridge.ParameterData : Type

Fixed parameter functions appearing in the scaled natural equations.

• A : ℝ

  A of ParameterData, of type ℝ.

• D : ℝ

  Domain data of ParameterData, of type ℝ.

• h : ℝ

  Step-size parameter of ParameterData, of type ℝ.

• chi : ℝ → ℝ

  Chi of ParameterData, of type ℝ → ℝ.

• d : ℝ → ℝ

  D of ParameterData, of type ℝ → ℝ.

• inverseL : ℝ → ℝ

  Inverse L of ParameterData, of type ℝ → ℝ.

• uStar : ℝ → ℝ

  U star of ParameterData, of type ℝ → ℝ.

• uStarEta : ℝ → ℝ

  U star eta of ParameterData, of type ℝ → ℝ.

• wStar : ℝ → ℝ

  W star of ParameterData, of type ℝ → ℝ.

• hStar : ℝ → ℝ

  H star of ParameterData, of type ℝ → ℝ.

• kappa : ℝ → ℝ

  Kappa of ParameterData, of type ℝ → ℝ.

• zStar : ℝ → ℝ

  Z star of ParameterData, of type ℝ → ℝ.

noncomputable def NavierStokes.NaturalAxisBridge.inputValue (I : AxisCoefficientSpace.Window) (ε : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) : ℝ → ℝ

The actual parameter function represented by the zeroth radial coefficient.

Equations

• NavierStokes.NaturalAxisBridge.inputValue I ε A = NavierStokes.AxisCoefficientSpace.coefficient I (NavierStokes.AxisWeightEstimates.weight ε) A 0

noncomputable def NavierStokes.NaturalAxisBridge.parameters (I : AxisCoefficientSpace.Window) (ε : ℝ) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (d : AxisContraction.AxisData ↥(AxisCoefficientSpace.AxisSpace I ε)) : ParameterData

The fixed fields of the integrated system, interpreted as actual functions.

Equations

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

structure NavierStokes.NaturalAxisBridge.CompatibleData (I : AxisCoefficientSpace.Window) (ε : ℝ) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (d : AxisContraction.AxisData ↥(AxisCoefficientSpace.AxisSpace I ε)) : Prop

Fixed analytic input data are independent of the radial coordinate. These hypotheses concern only the given inputs, never the unknown profiles.

• chi_radial : RadiallyConstant I ε χ
• one_radial : RadiallyConstant I ε d.one
• eta_radial : RadiallyConstant I ε d.eta
• d_radial : RadiallyConstant I ε d.d
• inverseL_radial : RadiallyConstant I ε d.inverseL
• uStar_radial : RadiallyConstant I ε d.uStar
• uStarEta_radial : RadiallyConstant I ε d.uStarEta
• wStar_radial : RadiallyConstant I ε d.wStar
• hStar_radial : RadiallyConstant I ε d.hStar
• gradient_radial : RadiallyConstant I ε d.normalizedGradient
• zStar_radial : RadiallyConstant I ε d.zStar
• one_value (η : ℝ) : η ∈ I.interval → inputValue I ε d.one η = 1
• eta_value (η : ℝ) : η ∈ I.interval → inputValue I ε d.eta η = η
• uStarEta_value (η : ℝ) : η ∈ Set.Ioo I.left I.right → inputValue I ε d.uStarEta η = deriv (inputValue I ε d.uStar) η

noncomputable def NavierStokes.NaturalAxisBridge.pressureSource (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (a Φ : ↥(AxisCoefficientSpace.AxisSpace I ε)) : ↥(AxisCoefficientSpace.AxisSpace I ε)

The pressure source in the complete coefficient space.

Equations

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

noncomputable def NavierStokes.NaturalAxisBridge.pressureCoefficient (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (a Φ : ↥(AxisCoefficientSpace.AxisSpace I ε)) : ↥(AxisCoefficientSpace.AxisSpace I ε)

Pressure coefficient, given by AxisOperators.primitive I hε (pressureSource I hε a Φ).

Equations

• NavierStokes.NaturalAxisBridge.pressureCoefficient I hε a Φ = (NavierStokes.AxisOperators.primitive I hε) (NavierStokes.NaturalAxisBridge.pressureSource I hε a Φ)

def NavierStokes.NaturalAxisBridge.reconstructedU (d : ParameterData) (t : ℝ) (u : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

The reconstructed axial profile U=U*+Λ⁻¹u.

Equations

• NavierStokes.NaturalAxisBridge.reconstructedU d t u p = d.uStar p.2 + t * u p

noncomputable def NavierStokes.NaturalAxisBridge.reconstructedW (d : ParameterData) (t : ℝ) (B : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

The actual transport coefficient using the regular radial average.

Equations

• NavierStokes.NaturalAxisBridge.reconstructedW d t B p = d.wStar p.2 - t * (2 * d.D * p.2 * B p + d.d p.2 * NavierStokes.NaturalAxisBridge.partialEta B p)

def NavierStokes.NaturalAxisBridge.reconstructedH (d : ParameterData) (t : ℝ) (u : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Reconstructed H, given by d.hStar p.2 + t * d.d p.2 * u p.

Equations

• NavierStokes.NaturalAxisBridge.reconstructedH d t u p = d.hStar p.2 + t * d.d p.2 * u p

noncomputable def NavierStokes.NaturalAxisBridge.angularRemainder (d : ParameterData) (t : ℝ) (Φ u B : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

The first remainder in equation (17), using ordinary derivatives of actual functions and κ=ξ₀/Λ.

Equations

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

noncomputable def NavierStokes.NaturalAxisBridge.axialRemainder (d : ParameterData) (t : ℝ) (u B P : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

The expanded second remainder in equation (17), including all pressure terms and the actual parameter derivative of the pressure correction.

Equations

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

structure NavierStokes.NaturalAxisBridge.IsScaledSolution (I : AxisCoefficientSpace.Window) (d : ParameterData) (t : ℝ) (a : ℝ → ℝ) (Φ u B P : ℝ × ℝ → ℝ) : Prop

The target is an equation for actual smooth profiles, together with the regular-average and pressure identities that determine its auxiliary fields.

• phi_smooth : ContDiffOn ℝ (↑⊤) Φ (AxisEvaluation.strip I 20)
• u_smooth : ContDiffOn ℝ (↑⊤) u (AxisEvaluation.strip I 20)
• average_smooth : ContDiffOn ℝ (↑⊤) B (AxisEvaluation.strip I 20)
• pressure_smooth : ContDiffOn ℝ (↑⊤) P (AxisEvaluation.strip I 20)
• phi_axis (η : ℝ) : η ∈ Set.Ioo I.left I.right → Φ (0, η) = 1
• u_axis (η : ℝ) : η ∈ Set.Ioo I.left I.right → u (0, η) = 0
• average_axis (η : ℝ) : η ∈ Set.Ioo I.left I.right → B (0, η) = u (0, η)
• pressure_axis (η : ℝ) : η ∈ Set.Ioo I.left I.right → P (0, η) = 0
• average_equation (p : ℝ × ℝ) : p ∈ AxisEvaluation.strip I 20 → B p + p.1 * partialY B p = u p
• pressure_equation (p : ℝ × ℝ) : p ∈ AxisEvaluation.strip I 20 → partialY P p = a p.2 ^ 2 * Φ p ^ 2
• average_integral (p : ℝ × ℝ) : p ∈ AxisEvaluation.strip I 20 → p.1 * B p = ∫ (y : ℝ) in 0..p.1, u (y, p.2)
• pressure_integral (p : ℝ × ℝ) : p ∈ AxisEvaluation.strip I 20 → P p = ∫ (y : ℝ) in 0..p.1, a p.2 ^ 2 * Φ (y, p.2) ^ 2
• angular_equation (p : ℝ × ℝ) : p ∈ AxisEvaluation.strip I 20 → 2 * radialDifferential 2 Φ p = -d.chi p.2 * Φ p + t * angularRemainder d t Φ u B p
• axial_equation (p : ℝ × ℝ) : p ∈ AxisEvaluation.strip I 20 → 2 * radialDifferential 1 u p = -d.inverseL p.2 * d.zStar p.2 + t * axialRemainder d t u B P p

theorem NavierStokes.NaturalAxisBridge.profile_inputValue (I : AxisCoefficientSpace.Window) (ε : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (hA : RadiallyConstant I ε A) {p : ℝ × ℝ} (hη : p.2 ∈ I.interval) : AxisEvaluation.profile I ε A p = inputValue I ε A p.2

theorem NavierStokes.NaturalAxisBridge.angular_remainder_evaluation (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (d : AxisContraction.AxisData ↥(AxisCoefficientSpace.AxisSpace I ε)) (hd : CompatibleData I ε χ d) (t : ℝ) (a : ↥(AxisCoefficientSpace.AxisSpace I ε)) (x : ↥(AxisCoefficientSpace.AxisSpace I ε) × ↥(AxisCoefficientSpace.AxisSpace I ε)) {p : ℝ × ℝ} (hp : p ∈ AxisEvaluation.strip I 20) : radialEvaluation I ε 2 (AxisContraction.naturalRemainder (AxisContraction.coefficientOperators I hε) d (ContinuousLinearMap.id ℝ ↥(AxisCoefficientSpace.AxisSpace I ε)) t a x).1 p = angularRemainder (parameters I ε χ d) t (AxisEvaluation.profile I ε x.1) (AxisEvaluation.profile I ε x.2) (AxisEvaluation.profile I ε ((AxisOperators.average I hε) x.2)) p

Differentiating the actual first integrated remainder gives precisely the first scaled differential remainder, including the mixed term.

theorem NavierStokes.NaturalAxisBridge.axial_remainder_evaluation (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (d : AxisContraction.AxisData ↥(AxisCoefficientSpace.AxisSpace I ε)) (hd : CompatibleData I ε χ d) (t : ℝ) (a : ↥(AxisCoefficientSpace.AxisSpace I ε)) (x : ↥(AxisCoefficientSpace.AxisSpace I ε) × ↥(AxisCoefficientSpace.AxisSpace I ε)) {p : ℝ × ℝ} (hp : p ∈ AxisEvaluation.strip I 20) : radialEvaluation I ε 1 (AxisContraction.naturalRemainder (AxisContraction.coefficientOperators I hε) d (ContinuousLinearMap.id ℝ ↥(AxisCoefficientSpace.AxisSpace I ε)) t a x).2 p = axialRemainder (parameters I ε χ d) t (AxisEvaluation.profile I ε x.2) (AxisEvaluation.profile I ε ((AxisOperators.average I hε) x.2)) (AxisEvaluation.profile I ε (pressureCoefficient I hε a x.1)) p

Differentiating the second integrated remainder gives the complete axial differential remainder, with the actual pressure derivatives.

theorem NavierStokes.NaturalAxisBridge.remainder_axis_zero (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (d : AxisContraction.AxisData ↥(AxisCoefficientSpace.AxisSpace I ε)) (t : ℝ) (a : ↥(AxisCoefficientSpace.AxisSpace I ε)) (x : ↥(AxisCoefficientSpace.AxisSpace I ε) × ↥(AxisCoefficientSpace.AxisSpace I ε)) {η : ℝ} (hη : η ∈ I.interval) : AxisEvaluation.profile I ε (AxisContraction.naturalRemainder (AxisContraction.coefficientOperators I hε) d (ContinuousLinearMap.id ℝ ↥(AxisCoefficientSpace.AxisSpace I ε)) t a x).1 (0, η) = 0 ∧ AxisEvaluation.profile I ε (AxisContraction.naturalRemainder (AxisContraction.coefficientOperators I hε) d (ContinuousLinearMap.id ℝ ↥(AxisCoefficientSpace.AxisSpace I ε)) t a x).2 (0, η) = 0

Both integrated remainders have exactly zero axis value.

theorem NavierStokes.NaturalAxisBridge.naturalOperator_axis_zero (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {η : ℝ} (hη : η ∈ I.interval) : AxisEvaluation.profile I ε ((AxisResolvent.naturalOperator I hε χ) A) (0, η) = 0

theorem NavierStokes.NaturalAxisBridge.radialEvaluation_naturalOperator (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (hχ : RadiallyConstant I ε χ) {p : ℝ × ℝ} (hp : p ∈ AxisEvaluation.strip I 20) : radialEvaluation I ε 2 ((AxisResolvent.naturalOperator I hε χ) A) p = 1 / 2 * inputValue I ε χ p.2 * AxisEvaluation.profile I ε A p

theorem NavierStokes.NaturalAxisBridge.pressure_equation (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (a Φ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (ha : RadiallyConstant I ε a) {p : ℝ × ℝ} (hp : p ∈ AxisEvaluation.strip I 20) : partialY (AxisEvaluation.profile I ε (pressureCoefficient I hε a Φ)) p = inputValue I ε a p.2 ^ 2 * AxisEvaluation.profile I ε Φ p ^ 2

theorem NavierStokes.NaturalAxisBridge.pressure_integral (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (a Φ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (ha : RadiallyConstant I ε a) {p : ℝ × ℝ} (hp : p ∈ AxisEvaluation.strip I 20) : AxisEvaluation.profile I ε (pressureCoefficient I hε a Φ) p = ∫ (y : ℝ) in 0..p.1, inputValue I ε a p.2 ^ 2 * AxisEvaluation.profile I ε Φ (y, p.2) ^ 2

The pressure field is the ordinary integral from the axis, rather than merely a formal coefficient primitive.

theorem NavierStokes.NaturalAxisBridge.integrated_solution (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (d : AxisContraction.AxisData ↥(AxisCoefficientSpace.AxisSpace I ε)) (hd : CompatibleData I ε χ d) (t s : ℝ) (hst : 2 * s = t) (a : ↥(AxisCoefficientSpace.AxisSpace I ε)) (ha : RadiallyConstant I ε a) (x : ↥(AxisCoefficientSpace.AxisSpace I ε) × ↥(AxisCoefficientSpace.AxisSpace I ε)) (hφ : x.1 + (AxisResolvent.naturalOperator I hε χ) x.1 = d.one + s • (AxisContraction.naturalRemainder (AxisContraction.coefficientOperators I hε) d (ContinuousLinearMap.id ℝ ↥(AxisCoefficientSpace.AxisSpace I ε)) t a x).1) (hu : x.2 = -(1 / 2) • (AxisOperators.regularInverse I hε 1 AxisContraction.coefficientOperators._proof_1) (((AxisOperators.product I hε) d.inverseL) d.zStar) + s • (AxisContraction.naturalRemainder (AxisContraction.coefficientOperators I hε) d (ContinuousLinearMap.id ℝ ↥(AxisCoefficientSpace.AxisSpace I ε)) t a x).2) : IsScaledSolution I (parameters I ε χ d) t (inputValue I ε a) (AxisEvaluation.profile I ε x.1) (AxisEvaluation.profile I ε x.2) (AxisEvaluation.profile I ε ((AxisOperators.average I hε) x.2)) (AxisEvaluation.profile I ε (pressureCoefficient I hε a x.1))

The integrated coefficient equations give the literal scaled equations for actual smooth functions on the open real strip.

noncomputable def NavierStokes.NaturalAxisBridge.referenceCoefficients (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (d : AxisContraction.AxisData ↥(AxisCoefficientSpace.AxisSpace I ε)) : ↥(AxisCoefficientSpace.AxisSpace I ε) × ↥(AxisCoefficientSpace.AxisSpace I ε)

The leading pair defined using the proved angular resolvent.

Equations

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

structure NavierStokes.NaturalAxisBridge.IsLeadingSolution (I : AxisCoefficientSpace.Window) (d : ParameterData) (Φ u : ℝ × ℝ → ℝ) : Prop

The limiting system is stated directly for actual functions.

• phi_smooth : ContDiffOn ℝ (↑⊤) Φ (AxisEvaluation.strip I 20)
• u_smooth : ContDiffOn ℝ (↑⊤) u (AxisEvaluation.strip I 20)
• phi_axis (η : ℝ) : η ∈ Set.Ioo I.left I.right → Φ (0, η) = 1
• u_axis (η : ℝ) : η ∈ Set.Ioo I.left I.right → u (0, η) = 0
• angular_equation (p : ℝ × ℝ) : p ∈ AxisEvaluation.strip I 20 → 2 * radialDifferential 2 Φ p = -d.chi p.2 * Φ p
• axial_equation (p : ℝ × ℝ) : p ∈ AxisEvaluation.strip I 20 → 2 * radialDifferential 1 u p = -d.inverseL p.2 * d.zStar p.2

theorem NavierStokes.NaturalAxisBridge.reference_isLeadingSolution (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (d : AxisContraction.AxisData ↥(AxisCoefficientSpace.AxisSpace I ε)) (hd : CompatibleData I ε χ d) : IsLeadingSolution I (parameters I ε χ d) (AxisEvaluation.profile I ε (referenceCoefficients I hε χ d).1) (AxisEvaluation.profile I ε (referenceCoefficients I hε χ d).2)

The profiles used in the error estimate really solve the regular leading equations with the prescribed axis data.

noncomputable def NavierStokes.NaturalAxisBridge.errorConstant (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (d : AxisContraction.AxisData ↥(AxisCoefficientSpace.AxisSpace I ε)) (M : ℝ) (hM : 0 ≤ M) : ℝ

A fixed finite constant computed from the input norms and the genuine bounded operators. It is independent of Λ and of the amplitude in its norm ball.

Equations

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

theorem NavierStokes.NaturalAxisBridge.errorConstant_nonneg (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (d : AxisContraction.AxisData ↥(AxisCoefficientSpace.AxisSpace I ε)) (M : ℝ) (hM : 0 ≤ M) : 0 ≤ errorConstant I hε χ d M hM

def NavierStokes.NaturalAxisBridge.UniformMixedError (I : AxisCoefficientSpace.Window) (ε K : ℝ) (Φ u Φ₀ u₀ : ℝ × ℝ → ℝ) : Prop

Simultaneous estimates for every ordinary mixed derivative, uniform on each smaller radial interval and on the whole open parameter interval.

Equations

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

theorem NavierStokes.NaturalAxisBridge.uniformMixedError_of_norm (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (x x₀ : ↥(AxisCoefficientSpace.AxisSpace I ε) × ↥(AxisCoefficientSpace.AxisSpace I ε)) (K : ℝ) (hK : ‖x - x₀‖ ≤ K) : UniformMixedError I ε K (AxisEvaluation.profile I ε x.1) (AxisEvaluation.profile I ε x.2) (AxisEvaluation.profile I ε x₀.1) (AxisEvaluation.profile I ε x₀.2)

theorem NavierStokes.NaturalAxisBridge.exists_scaled_profiles (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (d : AxisContraction.AxisData ↥(AxisCoefficientSpace.AxisSpace I ε)) (hd : CompatibleData I ε χ d) (M : ℝ) (hM : 0 ≤ M) : ∃ (Λ₀ : ℝ), 0 < Λ₀ ∧ ∀ (Λ : ℝ), Λ₀ ≤ Λ → ∀ (a : ↥(AxisCoefficientSpace.AxisSpace I ε)), ‖a‖ ≤ M → RadiallyConstant I ε a → ∃ (Φ : ℝ × ℝ → ℝ) (u : ℝ × ℝ → ℝ) (B : ℝ × ℝ → ℝ) (P : ℝ × ℝ → ℝ), IsScaledSolution I (parameters I ε χ d) (1 / Λ) (inputValue I ε a) Φ u B P ∧ UniformMixedError I ε (errorConstant I hε χ d M hM / (2 * Λ)) Φ u (AxisEvaluation.profile I ε (referenceCoefficients I hε χ d).1) (AxisEvaluation.profile I ε (referenceCoefficients I hε χ d).2)

Actual smooth natural-axis profiles exist for every sufficiently large Λ, uniformly over all radially constant angular amplitudes in a fixed norm ball. The conclusion is a differential/integral system for real functions, and its error estimate concerns their ordinary derivatives of every order.