Evaluation of the complete axis coefficient space

The evaluation series is constructed from the actual coefficient functions. Its mixed derivative series are proved convergent before their derivatives and smoothness are established.

def NavierStokes.AxisEvaluation.polynomialJet (n k : ℕ) (Y : ℝ) : ℝ

Polynomial jet, given by (n.descFactorial k : ℝ) * Y ^ (n - k).

Equations

• NavierStokes.AxisEvaluation.polynomialJet n k Y = ↑(n.descFactorial k) * Y ^ (n - k)

theorem NavierStokes.AxisEvaluation.polynomialJet_hasDerivAt (n k : ℕ) (Y : ℝ) : HasDerivAt (polynomialJet n k) (polynomialJet n (k + 1) Y) Y

noncomputable def NavierStokes.AxisEvaluation.term (I : AxisCoefficientSpace.Window) (ε : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m n : ℕ) (p : ℝ × ℝ) : ℝ

Term, given by polynomialJet n k p.1 * jet I (weight ε) A.1 n m p.2.

Equations

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

noncomputable def NavierStokes.AxisEvaluation.mixedSeries (I : AxisCoefficientSpace.Window) (ε : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m : ℕ) (p : ℝ × ℝ) : ℝ

Mixed series, given by ∑' n : ℕ, term I ε A k m n p.

Equations

• NavierStokes.AxisEvaluation.mixedSeries I ε A k m p = ∑' (n : ℕ), NavierStokes.AxisEvaluation.term I ε A k m n p

noncomputable def NavierStokes.AxisEvaluation.profile (I : AxisCoefficientSpace.Window) (ε : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (p : ℝ × ℝ) : ℝ

Profile, given by ∑' n : ℕ, p.1 ^ n * coefficient I (weight ε) A n p.2.

Equations

• NavierStokes.AxisEvaluation.profile I ε A p = ∑' (n : ℕ), p.1 ^ n * NavierStokes.AxisCoefficientSpace.coefficient I (NavierStokes.AxisWeightEstimates.weight ε) A n p.2

theorem NavierStokes.AxisEvaluation.mixedSeries_zero (I : AxisCoefficientSpace.Window) (ε : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) : mixedSeries I ε A 0 0 = profile I ε A

noncomputable def NavierStokes.AxisEvaluation.majorant (ε C R : ℝ) (k m n : ℕ) : ℝ

A deliberately simple polynomial-geometric majorant.

Equations

• NavierStokes.AxisEvaluation.majorant ε C R k m n = C * ε⁻¹ ^ m * ↑m.factorial * (↑m + 1) ^ m * ((↑n + 1) ^ (k + m) * (R / 20) ^ n)

theorem NavierStokes.AxisEvaluation.weight_upper {ε : ℝ} (hε : 0 < ε) (n m : ℕ) : AxisWeightEstimates.weight ε n m ≤ (1 / 20) ^ n * ε⁻¹ ^ m * ↑m.factorial * ((↑m + 1) ^ m * (↑n + 1) ^ m)

theorem NavierStokes.AxisEvaluation.polynomialJet_bound {R Y : ℝ} (hR : 1 ≤ R) (hY : |Y| ≤ R) (n k : ℕ) : |polynomialJet n k Y| ≤ (↑n + 1) ^ k * R ^ n

theorem NavierStokes.AxisEvaluation.term_bound (I : AxisCoefficientSpace.Window) {ε R : ℝ} (hε : 0 < ε) (hR : 1 ≤ R) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m n : ℕ) {p : ℝ × ℝ} (hp : |p.1| ≤ R) : ‖term I ε A k m n p‖ ≤ majorant ε ‖A‖ R k m n

theorem NavierStokes.AxisEvaluation.summable_majorant {ε C R : ℝ} (hR : 1 ≤ R) (hR20 : R < 20) (k m : ℕ) : Summable (majorant ε C R k m)

theorem NavierStokes.AxisEvaluation.summable_term (I : AxisCoefficientSpace.Window) {ε R : ℝ} (hε : 0 < ε) (hR : 1 ≤ R) (hR20 : R < 20) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m : ℕ) {p : ℝ × ℝ} (hp : |p.1| ≤ R) : Summable fun (n : ℕ) => term I ε A k m n p

theorem NavierStokes.AxisEvaluation.term_continuous (I : AxisCoefficientSpace.Window) (ε : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m n : ℕ) : Continuous (term I ε A k m n)

theorem NavierStokes.AxisEvaluation.mixedSeries_uniform (I : AxisCoefficientSpace.Window) {ε R : ℝ} (hε : 0 < ε) (hR20 : R < 20) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m : ℕ) : TendstoUniformlyOn (fun (N : ℕ) (p : ℝ × ℝ) => ∑ n ∈ Finset.range N, term I ε A k m n p) (mixedSeries I ε A k m) Filter.atTop {p : ℝ × ℝ | |p.1| ≤ R}

Uniform convergence of every mixed derivative series on every strictly smaller closed radial interval, uniformly over the parameter interval. In fact the clamped coefficient extension gives uniformity over all real η.

def NavierStokes.AxisEvaluation.strip (I : AxisCoefficientSpace.Window) (R : ℝ) : Set (ℝ × ℝ)

Strip, given by Ioo (-R) R ×ˢ Ioo I.left I.right.

Equations

• NavierStokes.AxisEvaluation.strip I R = Set.Ioo (-R) R ×ˢ Set.Ioo I.left I.right

theorem NavierStokes.AxisEvaluation.strip_isOpen (I : AxisCoefficientSpace.Window) (R : ℝ) : IsOpen (strip I R)

theorem NavierStokes.AxisEvaluation.strip_isPreconnected (I : AxisCoefficientSpace.Window) (R : ℝ) : IsPreconnected (strip I R)

def NavierStokes.AxisEvaluation.linearForm (u v : ℝ) : ℝ × ℝ →L[ℝ] ℝ

Linear form, given by u • ContinuousLinearMap.fst ℝ ℝ ℝ + v • ContinuousLinearMap.snd ℝ ℝ ℝ.

Equations

• NavierStokes.AxisEvaluation.linearForm u v = u • ContinuousLinearMap.fst ℝ ℝ ℝ + v • ContinuousLinearMap.snd ℝ ℝ ℝ

theorem NavierStokes.AxisEvaluation.linearForm_norm (u v : ℝ) : ‖linearForm u v‖ ≤ |u| + |v|

theorem NavierStokes.AxisEvaluation.term_hasFDerivAt (I : AxisCoefficientSpace.Window) (ε : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m n : ℕ) {p : ℝ × ℝ} (hp : p.2 ∈ Set.Ioo I.left I.right) : HasFDerivAt (term I ε A k m n) (linearForm (term I ε A (k + 1) m n p) (term I ε A k (m + 1) n p)) p

theorem NavierStokes.AxisEvaluation.linearForm_tsum {u v : ℕ → ℝ} (hu : Summable u) (hv : Summable v) : ∑' (n : ℕ), linearForm (u n) (v n) = linearForm (∑' (n : ℕ), u n) (∑' (n : ℕ), v n)

theorem NavierStokes.AxisEvaluation.mixedSeries_hasFDerivAt_strip (I : AxisCoefficientSpace.Window) {ε R : ℝ} (hε : 0 < ε) (hR : 1 ≤ R) (hR20 : R < 20) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m : ℕ) {p : ℝ × ℝ} (hp : p ∈ strip I R) : HasFDerivAt (mixedSeries I ε A k m) (linearForm (mixedSeries I ε A (k + 1) m p) (mixedSeries I ε A k (m + 1) p)) p

theorem NavierStokes.AxisEvaluation.mixedSeries_hasFDerivAt (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m : ℕ) {p : ℝ × ℝ} (hp : p ∈ strip I 20) : HasFDerivAt (mixedSeries I ε A k m) (linearForm (mixedSeries I ε A (k + 1) m p) (mixedSeries I ε A k (m + 1) p)) p

Actual joint differentiation of every mixed derivative series.

theorem NavierStokes.AxisEvaluation.mixedSeries_contDiffAt_nat (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (r k m : ℕ) (p : ℝ × ℝ) : p ∈ strip I 20 → ContDiffAt ℝ (↑r) (mixedSeries I ε A k m) p

theorem NavierStokes.AxisEvaluation.mixedSeries_smooth (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m : ℕ) {p : ℝ × ℝ} (hp : p ∈ strip I 20) : ContDiffAt ℝ (↑⊤) (mixedSeries I ε A k m) p

The evaluated profile is jointly smooth. This is a consequence of the proved derivative equations, not an assumed property of the infinite sum.

theorem NavierStokes.AxisEvaluation.profile_smooth (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) : ContDiffOn ℝ (↑⊤) (profile I ε A) (strip I 20)

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

theorem NavierStokes.AxisEvaluation.mixedSeries_hasDerivAt_eta (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m : ℕ) {Y η : ℝ} (hY : Y ∈ Set.Ioo (-20) 20) (hη : η ∈ Set.Ioo I.left I.right) : HasDerivAt (fun (x : ℝ) => mixedSeries I ε A k m (Y, x)) (mixedSeries I ε A k (m + 1) (Y, η)) η

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

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

theorem NavierStokes.AxisEvaluation.mixed_derivative_profile (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m : ℕ) {Y η : ℝ} (hY : Y ∈ Set.Ioo (-20) 20) (hη : η ∈ Set.Ioo I.left I.right) : iteratedDeriv m (fun (x : ℝ) => iteratedDeriv k (fun (y : ℝ) => profile I ε A (y, x)) Y) η = ∑' (n : ℕ), ↑(n.descFactorial k) * Y ^ (n - k) * AxisCoefficientSpace.jet I (AxisWeightEstimates.weight ε) (↑A) n m η

The series is the actual mixed derivative of the evaluated profile.

noncomputable def NavierStokes.AxisEvaluation.jetBound (ε R : ℝ) (k m : ℕ) : ℝ

Jet bound, given by ∑' n : ℕ, majorant ε 1 R k m n.

Equations

• NavierStokes.AxisEvaluation.jetBound ε R k m = ∑' (n : ℕ), NavierStokes.AxisEvaluation.majorant ε 1 R k m n

theorem NavierStokes.AxisEvaluation.majorant_scale (ε C R : ℝ) (k m n : ℕ) : majorant ε C R k m n = C * majorant ε 1 R k m n

theorem NavierStokes.AxisEvaluation.jetBound_nonneg {ε R : ℝ} (hε : 0 < ε) (hR : 1 ≤ R) (k m : ℕ) : 0 ≤ jetBound ε R k m

theorem NavierStokes.AxisEvaluation.mixedSeries_bound (I : AxisCoefficientSpace.Window) {ε R : ℝ} (hε : 0 < ε) (hR : 1 ≤ R) (hR20 : R < 20) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m : ℕ) {p : ℝ × ℝ} (hp : |p.1| ≤ R) : ‖mixedSeries I ε A k m p‖ ≤ jetBound ε R k m * ‖A‖

The evaluated mixed derivatives depend boundedly on the coefficient space norm, uniformly on every smaller radial interval.

theorem NavierStokes.AxisEvaluation.mixedSeries_summable (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m : ℕ) {p : ℝ × ℝ} (hp : |p.1| < 20) : Summable fun (n : ℕ) => term I ε A k m n p

Absolute convergence holds at every point of the radius-20 domain.

theorem NavierStokes.AxisEvaluation.profile_hasSum (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {p : ℝ × ℝ} (hp : |p.1| < 20) : HasSum (fun (n : ℕ) => p.1 ^ n * AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) A n p.2) (profile I ε A p)

theorem NavierStokes.AxisEvaluation.term_add (I : AxisCoefficientSpace.Window) (ε : ℝ) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m n : ℕ) (p : ℝ × ℝ) : term I ε (A + B) k m n p = term I ε A k m n p + term I ε B k m n p

theorem NavierStokes.AxisEvaluation.term_smul (I : AxisCoefficientSpace.Window) (ε c : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m n : ℕ) (p : ℝ × ℝ) : term I ε (c • A) k m n p = c * term I ε A k m n p

theorem NavierStokes.AxisEvaluation.term_sub (I : AxisCoefficientSpace.Window) (ε : ℝ) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m n : ℕ) (p : ℝ × ℝ) : term I ε (A - B) k m n p = term I ε A k m n p - term I ε B k m n p

theorem NavierStokes.AxisEvaluation.mixedSeries_add (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m : ℕ) {p : ℝ × ℝ} (hp : |p.1| < 20) : mixedSeries I ε (A + B) k m p = mixedSeries I ε A k m p + mixedSeries I ε B k m p

theorem NavierStokes.AxisEvaluation.mixedSeries_smul (I : AxisCoefficientSpace.Window) (ε c : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m : ℕ) (p : ℝ × ℝ) : mixedSeries I ε (c • A) k m p = c * mixedSeries I ε A k m p

theorem NavierStokes.AxisEvaluation.mixedSeries_sub (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m : ℕ) {p : ℝ × ℝ} (hp : |p.1| < 20) : mixedSeries I ε (A - B) k m p = mixedSeries I ε A k m p - mixedSeries I ε B k m p

noncomputable def NavierStokes.AxisEvaluation.evaluationLinearMap (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (k m : ℕ) (p : ℝ × ℝ) (hp : |p.1| < 20) : ↥(AxisCoefficientSpace.AxisSpace I ε) →ₗ[ℝ] ℝ

Evaluation linear map, bundling toFun, map_add, map_smul.

Equations

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

noncomputable def NavierStokes.AxisEvaluation.evaluationCLM (I : AxisCoefficientSpace.Window) {ε R : ℝ} (hε : 0 < ε) (hR : 1 ≤ R) (hR20 : R < 20) (k m : ℕ) (p : ℝ × ℝ) (hp : |p.1| ≤ R) : ↥(AxisCoefficientSpace.AxisSpace I ε) →L[ℝ] ℝ

Bounded evaluation of each actual mixed derivative from the complete coefficient space. The constant is uniform in the parameter coordinate.

Equations

• NavierStokes.AxisEvaluation.evaluationCLM I hε hR hR20 k m p hp = (NavierStokes.AxisEvaluation.evaluationLinearMap I hε k m p ⋯).mkContinuous (NavierStokes.AxisEvaluation.jetBound ε R k m) ⋯

@[simp]

theorem NavierStokes.AxisEvaluation.evaluationCLM_apply (I : AxisCoefficientSpace.Window) {ε R : ℝ} (hε : 0 < ε) (hR : 1 ≤ R) (hR20 : R < 20) (k m : ℕ) (p : ℝ × ℝ) (hp : |p.1| ≤ R) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) : (evaluationCLM I hε hR hR20 k m p hp) A = mixedSeries I ε A k m p

theorem NavierStokes.AxisEvaluation.mixedSeries_sub_bound (I : AxisCoefficientSpace.Window) {ε R : ℝ} (hε : 0 < ε) (hR : 1 ≤ R) (hR20 : R < 20) (A B : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m : ℕ) {p : ℝ × ℝ} (hp : |p.1| ≤ R) : ‖mixedSeries I ε A k m p - mixedSeries I ε B k m p‖ ≤ jetBound ε R k m * ‖A - B‖

Norm convergence in the coefficient space controls every evaluated jet uniformly throughout a smaller radial interval.

theorem NavierStokes.AxisEvaluation.profile_smooth_radius (I : AxisCoefficientSpace.Window) {ε R : ℝ} (hε : 0 < ε) (hR20 : R < 20) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) : ContDiffOn ℝ (↑⊤) (profile I ε A) (strip I R)

theorem NavierStokes.AxisEvaluation.coefficient_iteratedDeriv (I : AxisCoefficientSpace.Window) (ε : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n m : ℕ) {η : ℝ} (hη : η ∈ Set.Ioo I.left I.right) : iteratedDeriv m (AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) A n) η = AxisCoefficientSpace.jet I (AxisWeightEstimates.weight ε) (↑A) n m η

theorem NavierStokes.AxisEvaluation.mixed_derivative_profile_coefficients (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m : ℕ) {Y η : ℝ} (hY : Y ∈ Set.Ioo (-20) 20) (hη : η ∈ Set.Ioo I.left I.right) : iteratedDeriv m (fun (x : ℝ) => iteratedDeriv k (fun (y : ℝ) => profile I ε A (y, x)) Y) η = ∑' (n : ℕ), ↑(n.descFactorial k) * Y ^ (n - k) * iteratedDeriv m (AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) A n) η

Termwise mixed differentiation stated entirely using ordinary derivatives of the actual coefficient functions.

def NavierStokes.AxisEvaluation.enlargedUnitWindow (δ : ℝ) (hδ : 0 < δ) : AxisCoefficientSpace.Window

A window larger than the target interval, with arbitrarily small margin.

Equations

• NavierStokes.AxisEvaluation.enlargedUnitWindow δ hδ = { left := -1 - δ, right := 1 + δ, nondegenerate := ⋯ }

theorem NavierStokes.AxisEvaluation.unitInterval_in_enlargedWindow {δ : ℝ} (hδ : 0 < δ) : Set.Icc (-1) 1 ⊆ Set.Ioo (enlargedUnitWindow δ hδ).left (enlargedUnitWindow δ hδ).right

theorem NavierStokes.AxisEvaluation.profile_smooth_target {δ ε : ℝ} (hδ : 0 < δ) (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace (enlargedUnitWindow δ hδ) ε)) {Y η : ℝ} (hY : Y ∈ Set.Ioo (-20) 20) (hη : η ∈ Set.Icc (-1) 1) : ContDiffAt ℝ (↑⊤) (profile (enlargedUnitWindow δ hδ) ε A) (Y, η)

In particular both endpoints of the target interval [-1,1] have ordinary open-neighborhood smoothness; no endpoint extension is assumed.