A complete coefficient space with compatible actual derivatives

Normalized bounded continuous jets are restricted by closed, linear fundamental-theorem-of-calculus identities. Thus a point of the resulting Banach space determines genuine smooth coefficient functions, not unrelated arrays masquerading as their derivatives.

Concrete coefficient estimates for the natural-axis norm

Products are actual finite coefficient convolutions with the Leibniz binomial factors. In particular, the mixed derivative estimate is proved after the radial inverse; no boundedness of either differentiation operator on its own is assumed.

noncomputable def NavierStokes.AxisWeightEstimates.weight (ε : ℝ) (n m : ℕ) : ℝ

The exact coefficient weight printed in the candidate manuscript.

Equations

• NavierStokes.AxisWeightEstimates.weight ε n m = (1 / 20) ^ n * ε⁻¹ ^ m * ↑m.factorial * ↑((n + m).choose m) / ((↑n + 1) ^ 2 * (↑m + 1) ^ 2)

noncomputable def NavierStokes.AxisWeightEstimates.coreWeight (ε : ℝ) (n m : ℕ) : ℝ

The analytic part of the weight, before the two square-decay factors.

Equations

• NavierStokes.AxisWeightEstimates.coreWeight ε n m = (1 / 20) ^ n * ε⁻¹ ^ m * ↑m.factorial * ↑((n + m).choose m)

noncomputable def NavierStokes.AxisWeightEstimates.squareDecay (n : ℕ) : ℝ

Square decay, given by 1 / ((n : ℝ) + 1) ^ 2.

Equations

• NavierStokes.AxisWeightEstimates.squareDecay n = 1 / (↑n + 1) ^ 2

theorem NavierStokes.AxisWeightEstimates.weight_eq_core_decay (ε : ℝ) (n m : ℕ) : weight ε n m = coreWeight ε n m * squareDecay n * squareDecay m

theorem NavierStokes.AxisWeightEstimates.squareDecay_pos (n : ℕ) : 0 < squareDecay n

theorem NavierStokes.AxisWeightEstimates.coreWeight_pos {ε : ℝ} (hε : 0 < ε) (n m : ℕ) : 0 < coreWeight ε n m

theorem NavierStokes.AxisWeightEstimates.weight_pos {ε : ℝ} (hε : 0 < ε) (n m : ℕ) : 0 < weight ε n m

theorem NavierStokes.AxisWeightEstimates.squareDecay_succ_le (n : ℕ) : squareDecay (n + 1) ≤ squareDecay n

theorem NavierStokes.AxisWeightEstimates.squareDecay_le_four_succ (n : ℕ) : squareDecay n ≤ 4 * squareDecay (n + 1)

theorem NavierStokes.AxisWeightEstimates.reciprocal_square_telescope (x : ℝ) (hx : 1 ≤ x) : 1 / x ^ 2 ≤ 2 / x - 2 / (x + 1)

Elementary telescoping majorant for the square summability estimate.

theorem NavierStokes.AxisWeightEstimates.sum_squareDecay_le (n : ℕ) : ∑ i ∈ Finset.range (n + 1), squareDecay i ≤ 2 - 2 / (↑n + 2)

theorem NavierStokes.AxisWeightEstimates.sum_squareDecay_le_two (n : ℕ) : ∑ i ∈ Finset.range (n + 1), squareDecay i ≤ 2

theorem NavierStokes.AxisWeightEstimates.squareDecay_product_le (i j : ℕ) : squareDecay i * squareDecay j ≤ 2 * squareDecay (i + j) * (squareDecay i + squareDecay j)

theorem NavierStokes.AxisWeightEstimates.squareDecay_convolution_le (n : ℕ) : ∑ ij ∈ Finset.antidiagonal n, squareDecay ij.1 * squareDecay ij.2 ≤ 8 * squareDecay n

The one-dimensional convolution constant is at most eight.

theorem NavierStokes.AxisWeightEstimates.choose_product_le (i j k l : ℕ) : (i + k).choose k * (j + l).choose l ≤ (i + j + (k + l)).choose (k + l)

A term of Vandermonde's sum gives the binomial estimate used in the norm.

theorem NavierStokes.AxisWeightEstimates.choose_factorials (k l : ℕ) : ↑((k + l).choose k) * ↑k.factorial * ↑l.factorial = ↑(k + l).factorial

theorem NavierStokes.AxisWeightEstimates.coreWeight_product_le {ε : ℝ} (hε : 0 < ε) (i j k l : ℕ) : ↑((k + l).choose k) * coreWeight ε i k * coreWeight ε j l ≤ coreWeight ε (i + j) (k + l)

The analytic factors respect the Leibniz convolution with constant one.

theorem NavierStokes.AxisWeightEstimates.coreWeight_factorial (ε : ℝ) (n m : ℕ) : coreWeight ε n m = (1 / 20) ^ n * ε⁻¹ ^ m * ↑(n + m).factorial / ↑n.factorial

Factorial form used only to prove the exact shift identities.

theorem NavierStokes.AxisWeightEstimates.coreWeight_radial_identity {ε : ℝ} (hε : 0 < ε) (n m : ℕ) : coreWeight ε n m * (↑n + ↑m + 1) = 20 * (↑n + 1) * coreWeight ε (n + 1) m

theorem NavierStokes.AxisWeightEstimates.coreWeight_radial_le {ε : ℝ} (hε : 0 < ε) (n m : ℕ) : coreWeight ε n m ≤ 20 * coreWeight ε (n + 1) m

theorem NavierStokes.AxisWeightEstimates.coreWeight_parameter_shift {ε : ℝ} (hε : 0 < ε) (i k : ℕ) : coreWeight ε i (k + 1) = 20 / ε * (↑i + 1) * coreWeight ε (i + 1) k

theorem NavierStokes.AxisWeightEstimates.weight_radial_shift {ε : ℝ} (hε : 0 < ε) (n m : ℕ) : weight ε n m ≤ 80 * weight ε (n + 1) m

A radial shift costs at most the printed factor 4 * 20 = 80.

theorem NavierStokes.AxisWeightEstimates.weight_radial_shift_ratio {ε : ℝ} (hε : 0 < ε) (n m : ℕ) : weight ε n m / weight ε (n + 1) m ≤ 80

theorem NavierStokes.AxisWeightEstimates.weight_parameter_radial_shift {ε : ℝ} (hε : 0 < ε) (i k : ℕ) : weight ε i (k + 1) ≤ 80 / ε * (↑i + 1) * weight ε (i + 1) k

Assigning the output radial shift to a parameter-differentiated factor.

theorem NavierStokes.AxisWeightEstimates.weight_parameter_radial_shift_ratio {ε : ℝ} (hε : 0 < ε) (i k : ℕ) : weight ε i (k + 1) / weight ε (i + 1) k ≤ 80 / ε * (↑i + 1)

noncomputable def NavierStokes.AxisWeightEstimates.productWeightSum (ε : ℝ) (n m : ℕ) : ℝ

The finite weight convolution associated with radial multiplication and the parameter Leibniz rule.

Equations

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

theorem NavierStokes.AxisWeightEstimates.weight_product_term_le {ε : ℝ} (hε : 0 < ε) (i j k l : ℕ) : ↑((k + l).choose k) * weight ε i k * weight ε j l ≤ coreWeight ε (i + j) (k + l) * (squareDecay i * squareDecay j) * (squareDecay k * squareDecay l)

theorem NavierStokes.AxisWeightEstimates.productWeightSum_le {ε : ℝ} (hε : 0 < ε) (n m : ℕ) : productWeightSum ε n m ≤ 64 * weight ε n m

The manuscript's uniform algebra constant 64, with actual finite sums.

def NavierStokes.AxisWeightEstimates.jetProduct (f g : ℕ → ℕ → ℝ) (n m : ℕ) : ℝ

Actual radial convolution with the parameter Leibniz coefficients.

Equations

• NavierStokes.AxisWeightEstimates.jetProduct f g n m = ∑ ij ∈ Finset.antidiagonal n, ∑ kl ∈ Finset.antidiagonal m, ↑(m.choose kl.1) * f ij.1 kl.1 * g ij.2 kl.2

theorem NavierStokes.AxisWeightEstimates.abs_bilinear_term_le (a x y wx wy F G : ℝ) (ha : 0 ≤ a) (hF : 0 ≤ F) (_hG : 0 ≤ G) (hwx : 0 ≤ wx) (_hwy : 0 ≤ wy) (hx : |x| ≤ F * wx) (hy : |y| ≤ G * wy) : |a * x * y| ≤ F * G * (a * wx * wy)

theorem NavierStokes.AxisWeightEstimates.abs_double_sum_le {ι : Type u_1} {κ : Type u_2} (s : Finset ι) (t : Finset κ) (f M : ι → κ → ℝ) (h : ∀ i ∈ s, ∀ k ∈ t, |f i k| ≤ M i k) : |∑ i ∈ s, ∑ k ∈ t, f i k| ≤ ∑ i ∈ s, ∑ k ∈ t, M i k

theorem NavierStokes.AxisWeightEstimates.jetProduct_bound {ε F G : ℝ} (hε : 0 < ε) (hF : 0 ≤ F) (hG : 0 ≤ G) (f g : ℕ → ℕ → ℝ) (hf : ∀ (n m : ℕ), |f n m| ≤ F * weight ε n m) (hg : ∀ (n m : ℕ), |g n m| ≤ G * weight ε n m) (n m : ℕ) : |jetProduct f g n m| ≤ 64 * F * G * weight ε n m

Uniform coefficient product bound, requiring only the actual coefficient bounds on the two input arrays.

def NavierStokes.AxisWeightEstimates.radialDivisor (r n : ℕ) : ℝ

Radial divisor, given by ((n : ℝ) + 1) * ((n : ℝ) + r).

Equations

• NavierStokes.AxisWeightEstimates.radialDivisor r n = (↑n + 1) * (↑n + ↑r)

theorem NavierStokes.AxisWeightEstimates.radialDivisor_pos {r : ℕ} (hr : 1 ≤ r) (n : ℕ) : 0 < radialDivisor r n

theorem NavierStokes.AxisWeightEstimates.mixed_factors_le_divisor {r n i j : ℕ} (hr : 1 ≤ r) (hij : i + j = n) : (↑i + 1) * ↑j ≤ radialDivisor r n

The extra parameter and dot factors fit inside the regular radial divisor.

noncomputable def NavierStokes.AxisWeightEstimates.shiftedProductWeightSum (ε : ℝ) (n m : ℕ) : ℝ

Shifted product weight sum, given by ∑ ij ∈ antidiagonal n, ∑ kl ∈ antidiagonal m, (m.choose kl.1 : ℝ) * weight ε (ij.1 + 1) kl.1 * weight ε ij.2 kl.2.

Equations

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

theorem NavierStokes.AxisWeightEstimates.shiftedProductWeightSum_le {ε : ℝ} (hε : 0 < ε) (n m : ℕ) : shiftedProductWeightSum ε n m ≤ 64 * weight ε (n + 1) m

theorem NavierStokes.AxisWeightEstimates.mixed_weight_term_le {ε : ℝ} (hε : 0 < ε) {r n i j : ℕ} (hr : 1 ≤ r) (hij : i + j = n) (m k l : ℕ) : ↑(m.choose k) * ↑j / radialDivisor r n * weight ε i (k + 1) * weight ε j l ≤ 80 / ε * (↑(m.choose k) * weight ε (i + 1) k * weight ε j l)

A single mixed term after applying the inverse radial divisor.

noncomputable def NavierStokes.AxisWeightEstimates.mixedWeightSum (ε : ℝ) (r n m : ℕ) : ℝ

Mixed weight sum, choosing the witness provided by kl.1.

Equations

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

theorem NavierStokes.AxisWeightEstimates.mixedWeightSum_le {ε : ℝ} (hε : 0 < ε) {r : ℕ} (hr : 1 ≤ r) (n m : ℕ) : mixedWeightSum ε r n m ≤ 5120 / ε * weight ε (n + 1) m

noncomputable def NavierStokes.AxisWeightEstimates.inverseMixedJet (r : ℕ) (f g : ℕ → ℕ → ℝ) (n m : ℕ) : ℝ

The coefficient at radial degree n+1 of J_r((∂η f) D_Y g). The radial divisor is distributed over its finite convolution sum.

Equations

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

theorem NavierStokes.AxisWeightEstimates.inverseMixedJet_bound {ε F G : ℝ} (hε : 0 < ε) (hF : 0 ≤ F) (hG : 0 ≤ G) {r : ℕ} (hr : 1 ≤ r) (f g : ℕ → ℕ → ℝ) (hf : ∀ (n m : ℕ), |f n m| ≤ F * weight ε n m) (hg : ∀ (n m : ℕ), |g n m| ≤ G * weight ε n m) (n m : ℕ) : |inverseMixedJet r f g n m| ≤ 5120 / ε * F * G * weight ε (n + 1) m

The mixed derivative is bounded after radial inversion, with explicit constant 5120/ε. Neither individual derivative is assumed bounded.

noncomputable def NavierStokes.AxisWeightEstimates.averageJet (f : ℕ → ℕ → ℝ) (n m : ℕ) : ℝ

Coefficients of the radial averaging operator Bf(Y)=∫₀¹ f(tY)dt.

Equations

• NavierStokes.AxisWeightEstimates.averageJet f n m = f n m / (↑n + 1)

noncomputable def NavierStokes.AxisWeightEstimates.primitiveJet (f : ℕ → ℕ → ℝ) : ℕ → ℕ → ℝ

Coefficients of the zero-datum primitive.

Equations

• NavierStokes.AxisWeightEstimates.primitiveJet f 0 x✝ = 0
• NavierStokes.AxisWeightEstimates.primitiveJet f n.succ x✝ = f n x✝ / (↑n + 1)

noncomputable def NavierStokes.AxisWeightEstimates.regularInverseJet (r : ℕ) (f : ℕ → ℕ → ℝ) : ℕ → ℕ → ℝ

Coefficients of the regular zero-datum inverse of Y f'' + r f'.

Equations

• NavierStokes.AxisWeightEstimates.regularInverseJet r f 0 x✝ = 0
• NavierStokes.AxisWeightEstimates.regularInverseJet r f n.succ x✝ = f n x✝ / NavierStokes.AxisWeightEstimates.radialDivisor r n

noncomputable def NavierStokes.AxisWeightEstimates.parameterPrimitiveJet (f : ℕ → ℕ → ℝ) : ℕ → ℕ → ℝ

The primitive is applied together with the parameter derivative.

Equations

• NavierStokes.AxisWeightEstimates.parameterPrimitiveJet f 0 x✝ = 0
• NavierStokes.AxisWeightEstimates.parameterPrimitiveJet f n.succ x✝ = f n (x✝ + 1) / (↑n + 1)

theorem NavierStokes.AxisWeightEstimates.averageJet_bound {ε F : ℝ} (_hε : 0 < ε) (_hF : 0 ≤ F) (f : ℕ → ℕ → ℝ) (hf : ∀ (n m : ℕ), |f n m| ≤ F * weight ε n m) (n m : ℕ) : |averageJet f n m| ≤ F * weight ε n m

theorem NavierStokes.AxisWeightEstimates.primitiveJet_bound {ε F : ℝ} (hε : 0 < ε) (hF : 0 ≤ F) (f : ℕ → ℕ → ℝ) (hf : ∀ (n m : ℕ), |f n m| ≤ F * weight ε n m) (n m : ℕ) : |primitiveJet f n m| ≤ 80 * F * weight ε n m

theorem NavierStokes.AxisWeightEstimates.radialDivisor_ge_one {r : ℕ} (hr : 1 ≤ r) (n : ℕ) : 1 ≤ radialDivisor r n

theorem NavierStokes.AxisWeightEstimates.regularInverseJet_bound {ε F : ℝ} (hε : 0 < ε) (hF : 0 ≤ F) {r : ℕ} (hr : 1 ≤ r) (f : ℕ → ℕ → ℝ) (hf : ∀ (n m : ℕ), |f n m| ≤ F * weight ε n m) (n m : ℕ) : |regularInverseJet r f n m| ≤ 80 * F * weight ε n m

theorem NavierStokes.AxisWeightEstimates.parameterPrimitiveJet_bound {ε F : ℝ} (hε : 0 < ε) (hF : 0 ≤ F) (f : ℕ → ℕ → ℝ) (hf : ∀ (n m : ℕ), |f n m| ≤ F * weight ε n m) (n m : ℕ) : |parameterPrimitiveJet f n m| ≤ 80 / ε * F * weight ε n m

noncomputable def NavierStokes.AxisWeightEstimates.regularInverseMixedJet (r : ℕ) (f g : ℕ → ℕ → ℝ) : ℕ → ℕ → ℝ

Put the already estimated mixed coefficient in its output radial degree.

Equations

• NavierStokes.AxisWeightEstimates.regularInverseMixedJet r f g 0 x✝ = 0
• NavierStokes.AxisWeightEstimates.regularInverseMixedJet r f g n.succ x✝ = NavierStokes.AxisWeightEstimates.inverseMixedJet r f g n x✝

theorem NavierStokes.AxisWeightEstimates.regularInverseMixedJet_bound {ε F G : ℝ} (hε : 0 < ε) (hF : 0 ≤ F) (hG : 0 ≤ G) {r : ℕ} (hr : 1 ≤ r) (f g : ℕ → ℕ → ℝ) (hf : ∀ (n m : ℕ), |f n m| ≤ F * weight ε n m) (hg : ∀ (n m : ℕ), |g n m| ≤ G * weight ε n m) (n m : ℕ) : |regularInverseMixedJet r f g n m| ≤ 5120 / ε * F * G * weight ε n m

structure NavierStokes.AxisCoefficientSpace.Window : Type

A fixed nondegenerate compact real parameter interval.

• left : ℝ

  Left of Window, of type ℝ.

• right : ℝ

  Right of Window, of type ℝ.

• nondegenerate : self.left < self.right

def NavierStokes.AxisCoefficientSpace.Window.interval (I : Window) : Set ℝ

Interval, given by Icc I.left I.right.

Equations

• I.interval = Set.Icc I.left I.right

noncomputable def NavierStokes.AxisCoefficientSpace.Window.project (I : Window) : ℝ → ↑I.interval

The continuous clamping map is only an extension device. Smoothness is proved on the original closed interval, including its one-sided endpoint jets.

Equations

• I.project = Set.projIcc I.left I.right ⋯

theorem NavierStokes.AxisCoefficientSpace.Window.continuous_project (I : Window) : Continuous I.project

theorem NavierStokes.AxisCoefficientSpace.Window.project_of_mem (I : Window) {x : ℝ} (hx : x ∈ I.interval) : I.project x = ⟨x, hx⟩

@[reducible, inline]

abbrev NavierStokes.AxisCoefficientSpace.RawJets (I : Window) : Type

Ambient normalized jets with the supremum norm over both indices and the compact parameter interval.

Equations

• NavierStokes.AxisCoefficientSpace.RawJets I = BoundedContinuousFunction ((ℕ × ℕ) × ↑I.interval) ℝ

noncomputable def NavierStokes.AxisCoefficientSpace.jet (I : Window) (w : ℕ → ℕ → ℝ) (A : RawJets I) (n m : ℕ) (x : ℝ) : ℝ

Unnormalized, continuously extended m-th jet of coefficient n.

Equations

• NavierStokes.AxisCoefficientSpace.jet I w A n m x = w n m * A ((n, m), I.project x)

theorem NavierStokes.AxisCoefficientSpace.continuous_jet (I : Window) (w : ℕ → ℕ → ℝ) (A : RawJets I) (n m : ℕ) : Continuous (jet I w A n m)

theorem NavierStokes.AxisCoefficientSpace.continuous_jet_parameter (I : Window) (w : ℕ → ℕ → ℝ) (n m : ℕ) (x : ℝ) : Continuous fun (A : RawJets I) => jet I w A n m x

theorem NavierStokes.AxisCoefficientSpace.continuous_jet_joint (I : Window) (w : ℕ → ℕ → ℝ) (n m : ℕ) : Continuous fun (p : RawJets I × ℝ) => jet I w p.1 n m p.2

@[simp]

theorem NavierStokes.AxisCoefficientSpace.jet_zero (I : Window) (w : ℕ → ℕ → ℝ) (n m : ℕ) (x : ℝ) : jet I w 0 n m x = 0

@[simp]

theorem NavierStokes.AxisCoefficientSpace.jet_add (I : Window) (w : ℕ → ℕ → ℝ) (A B : RawJets I) (n m : ℕ) (x : ℝ) : jet I w (A + B) n m x = jet I w A n m x + jet I w B n m x

@[simp]

theorem NavierStokes.AxisCoefficientSpace.jet_sub (I : Window) (w : ℕ → ℕ → ℝ) (A B : RawJets I) (n m : ℕ) (x : ℝ) : jet I w (A - B) n m x = jet I w A n m x - jet I w B n m x

@[simp]

theorem NavierStokes.AxisCoefficientSpace.jet_smul (I : Window) (w : ℕ → ℕ → ℝ) (c : ℝ) (A : RawJets I) (n m : ℕ) (x : ℝ) : jet I w (c • A) n m x = c * jet I w A n m x

def NavierStokes.AxisCoefficientSpace.Compatible (I : Window) (w : ℕ → ℕ → ℝ) (A : RawJets I) : Prop

Compatibility is an actual FTC identity for every successive pair of jets, throughout the full interval.

Equations

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

def NavierStokes.AxisCoefficientSpace.compatibleSubmodule (I : Window) (w : ℕ → ℕ → ℝ) : Submodule ℝ (RawJets I)

The compatible arrays form a linear subspace of the ambient Banach space.

Equations

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

theorem NavierStokes.AxisCoefficientSpace.isClosed_compatible (I : Window) (w : ℕ → ℕ → ℝ) : IsClosed {A : RawJets I | Compatible I w A}

Closedness follows from continuous evaluation and continuous interval integration. This is the completeness-critical compatibility argument.

@[reducible, inline]

abbrev NavierStokes.AxisCoefficientSpace.CoefficientSpace (I : Window) (w : ℕ → ℕ → ℝ) : Submodule ℝ (RawJets I)

The coefficient space, retaining the inherited genuine norm and linear structure.

Equations

• NavierStokes.AxisCoefficientSpace.CoefficientSpace I w = NavierStokes.AxisCoefficientSpace.compatibleSubmodule I w

instance NavierStokes.AxisCoefficientSpace.coefficientSpace_complete (I : Window) (w : ℕ → ℕ → ℝ) : CompleteSpace ↥(CoefficientSpace I w)

noncomputable def NavierStokes.AxisCoefficientSpace.coefficient (I : Window) (w : ℕ → ℕ → ℝ) (A : ↥(CoefficientSpace I w)) (n : ℕ) : ℝ → ℝ

A coefficient is the zeroth actual jet.

Equations

• NavierStokes.AxisCoefficientSpace.coefficient I w A n = NavierStokes.AxisCoefficientSpace.jet I w (↑A) n 0

theorem NavierStokes.AxisCoefficientSpace.hasDerivWithinAt_jet (I : Window) (w : ℕ → ℕ → ℝ) (A : ↥(CoefficientSpace I w)) (n m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : HasDerivWithinAt (jet I w (↑A) n m) (jet I w (↑A) n (m + 1) x) I.interval x

FTC compatibility identifies the derivative within the closed interval; this includes the corresponding one-sided endpoint derivatives.

theorem NavierStokes.AxisCoefficientSpace.derivWithin_jet (I : Window) (w : ℕ → ℕ → ℝ) (A : ↥(CoefficientSpace I w)) (n m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : derivWithin (jet I w (↑A) n m) I.interval x = jet I w (↑A) n (m + 1) x

theorem NavierStokes.AxisCoefficientSpace.hasDerivAt_jet_interior (I : Window) (w : ℕ → ℕ → ℝ) (A : ↥(CoefficientSpace I w)) (n m : ℕ) {x : ℝ} (hx : x ∈ Set.Ioo I.left I.right) : HasDerivAt (jet I w (↑A) n m) (jet I w (↑A) n (m + 1) x) x

At every interior point these are the ordinary real derivatives.

theorem NavierStokes.AxisCoefficientSpace.iteratedDerivWithin_jet (I : Window) (w : ℕ → ℕ → ℝ) (A : ↥(CoefficientSpace I w)) (n q m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : iteratedDerivWithin m (jet I w (↑A) n q) I.interval x = jet I w (↑A) n (q + m) x

Every stored jet is the corresponding iterated derivative of the actual function.

theorem NavierStokes.AxisCoefficientSpace.iteratedDerivWithin_coefficient (I : Window) (w : ℕ → ℕ → ℝ) (A : ↥(CoefficientSpace I w)) (n m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : iteratedDerivWithin m (coefficient I w A n) I.interval x = jet I w (↑A) n m x

theorem NavierStokes.AxisCoefficientSpace.contDiffOn_jet (I : Window) (w : ℕ → ℕ → ℝ) (A : ↥(CoefficientSpace I w)) (n q : ℕ) : ContDiffOn ℝ (↑⊤) (jet I w (↑A) n q) I.interval

Genuine infinite smoothness on the full compact interval.

theorem NavierStokes.AxisCoefficientSpace.contDiffOn_coefficient (I : Window) (w : ℕ → ℕ → ℝ) (A : ↥(CoefficientSpace I w)) (n : ℕ) : ContDiffOn ℝ (↑⊤) (coefficient I w A n) I.interval

theorem NavierStokes.AxisCoefficientSpace.contDiffAt_coefficient_interior (I : Window) (w : ℕ → ℕ → ℝ) (A : ↥(CoefficientSpace I w)) (n : ℕ) {x : ℝ} (hx : x ∈ Set.Ioo I.left I.right) : ContDiffAt ℝ (↑⊤) (coefficient I w A n) x

On the interior these are ordinary smooth real functions on an open neighborhood, so an original interval may be placed inside this enlarged one.

theorem NavierStokes.AxisCoefficientSpace.abs_jet_le (I : Window) (w : ℕ → ℕ → ℝ) (A : ↥(CoefficientSpace I w)) (n m : ℕ) (x : ℝ) : |jet I w (↑A) n m x| ≤ |w n m| * ‖A‖

The inherited norm controls every actual parameter derivative with its weight.

theorem NavierStokes.AxisCoefficientSpace.abs_iteratedDerivWithin_coefficient_le (I : Window) (w : ℕ → ℕ → ℝ) (A : ↥(CoefficientSpace I w)) (n m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : |iteratedDerivWithin m (coefficient I w A n) I.interval x| ≤ |w n m| * ‖A‖

theorem NavierStokes.AxisCoefficientSpace.abs_jet_sub_le (I : Window) (w : ℕ → ℕ → ℝ) (A B : ↥(CoefficientSpace I w)) (n m : ℕ) (x : ℝ) : |jet I w (↑A) n m x - jet I w (↑B) n m x| ≤ |w n m| * ‖A - B‖

Norm convergence controls every derivative uniformly in the parameter.

theorem NavierStokes.AxisCoefficientSpace.normalized_derivative (I : Window) (w : ℕ → ℕ → ℝ) (hw : ∀ (n m : ℕ), w n m ≠ 0) (A : ↥(CoefficientSpace I w)) (n m : ℕ) (x : ↑I.interval) : iteratedDerivWithin m (coefficient I w A n) I.interval ↑x / w n m = ↑A ((n, m), x)

For nonzero weights, the normalized actual derivative recovers exactly the stored bounded-continuous coordinate.

theorem NavierStokes.AxisCoefficientSpace.quotient_abs_derivative (I : Window) (w : ℕ → ℕ → ℝ) (hw : ∀ (n m : ℕ), 0 < w n m) (A : ↥(CoefficientSpace I w)) (n m : ℕ) (x : ↑I.interval) : |iteratedDerivWithin m (coefficient I w A n) I.interval ↑x| / w n m = |↑A ((n, m), x)|

theorem NavierStokes.AxisCoefficientSpace.norm_le_iff_derivative_bound (I : Window) (w : ℕ → ℕ → ℝ) (hw : ∀ (n m : ℕ), 0 < w n m) (A : ↥(CoefficientSpace I w)) (C : ℝ) (hC : 0 ≤ C) : ‖A‖ ≤ C ↔ ∀ (n m : ℕ) (x : ↑I.interval), |iteratedDerivWithin m (coefficient I w A n) I.interval ↑x| / w n m ≤ C

This is precisely the supremum quotient norm in the manuscript, expressed by its universal upper-bound characterization.

theorem NavierStokes.AxisCoefficientSpace.coefficient_ext (I : Window) (w : ℕ → ℕ → ℝ) (hw : ∀ (n m : ℕ), w n m ≠ 0) (A B : ↥(CoefficientSpace I w)) (h : ∀ (n : ℕ), ∀ x ∈ I.interval, coefficient I w A n x = coefficient I w B n x) : A = B

Positive weights leave no independent or invisible jet coordinates: equality of the actual coefficient functions forces equality in the space.

noncomputable def NavierStokes.AxisCoefficientSpace.rawOfJetFamily (I : Window) (w : ℕ → ℕ → ℝ) (hw : ∀ (n m : ℕ), 0 < w n m) (J : ℕ → ℕ → ℝ → ℝ) (hcont : ∀ (n m : ℕ), ContinuousOn (J n m) I.interval) (C : ℝ) (hbound : ∀ (n m : ℕ), ∀ x ∈ I.interval, |J n m x| ≤ C * w n m) : RawJets I

Normalize an actual continuous jet family with a uniform weighted bound.

Equations

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

theorem NavierStokes.AxisCoefficientSpace.jet_rawOfJetFamily (I : Window) (w : ℕ → ℕ → ℝ) (hw : ∀ (n m : ℕ), 0 < w n m) (J : ℕ → ℕ → ℝ → ℝ) (hcont : ∀ (n m : ℕ), ContinuousOn (J n m) I.interval) (C : ℝ) (hbound : ∀ (n m : ℕ), ∀ x ∈ I.interval, |J n m x| ≤ C * w n m) (n m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : jet I w (rawOfJetFamily I w hw J hcont C hbound) n m x = J n m x

theorem NavierStokes.AxisCoefficientSpace.compatible_rawOfJetFamily (I : Window) (w : ℕ → ℕ → ℝ) (hw : ∀ (n m : ℕ), 0 < w n m) (J : ℕ → ℕ → ℝ → ℝ) (hcont : ∀ (n m : ℕ), ContinuousOn (J n m) I.interval) (hderiv : ∀ (n m : ℕ), ∀ x ∈ I.interval, HasDerivWithinAt (J n m) (J n (m + 1) x) I.interval x) (C : ℝ) (hbound : ∀ (n m : ℕ), ∀ x ∈ I.interval, |J n m x| ≤ C * w n m) : Compatible I w (rawOfJetFamily I w hw J hcont C hbound)

Actual derivative compatibility implies the closed FTC compatibility required by the Banach-space representation.

noncomputable def NavierStokes.AxisCoefficientSpace.ofJetFamily (I : Window) (w : ℕ → ℕ → ℝ) (hw : ∀ (n m : ℕ), 0 < w n m) (J : ℕ → ℕ → ℝ → ℝ) (hcont : ∀ (n m : ℕ), ContinuousOn (J n m) I.interval) (hderiv : ∀ (n m : ℕ), ∀ x ∈ I.interval, HasDerivWithinAt (J n m) (J n (m + 1) x) I.interval x) (C : ℝ) (_hC : 0 ≤ C) (hbound : ∀ (n m : ℕ), ∀ x ∈ I.interval, |J n m x| ≤ C * w n m) : ↥(CoefficientSpace I w)

Reverse constructor used by genuine products and radial operators: a continuous family with actual adjacent derivatives and the weighted bound becomes an element of the complete coefficient space.

Equations

• NavierStokes.AxisCoefficientSpace.ofJetFamily I w hw J hcont hderiv C _hC hbound = ⟨NavierStokes.AxisCoefficientSpace.rawOfJetFamily I w hw J hcont C hbound, ⋯⟩

theorem NavierStokes.AxisCoefficientSpace.jet_ofJetFamily (I : Window) (w : ℕ → ℕ → ℝ) (hw : ∀ (n m : ℕ), 0 < w n m) (J : ℕ → ℕ → ℝ → ℝ) (hcont : ∀ (n m : ℕ), ContinuousOn (J n m) I.interval) (hderiv : ∀ (n m : ℕ), ∀ x ∈ I.interval, HasDerivWithinAt (J n m) (J n (m + 1) x) I.interval x) (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ (n m : ℕ), ∀ x ∈ I.interval, |J n m x| ≤ C * w n m) (n m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : jet I w (↑(ofJetFamily I w hw J hcont hderiv C hC hbound)) n m x = J n m x

theorem NavierStokes.AxisCoefficientSpace.coefficient_ofJetFamily (I : Window) (w : ℕ → ℕ → ℝ) (hw : ∀ (n m : ℕ), 0 < w n m) (J : ℕ → ℕ → ℝ → ℝ) (hcont : ∀ (n m : ℕ), ContinuousOn (J n m) I.interval) (hderiv : ∀ (n m : ℕ), ∀ x ∈ I.interval, HasDerivWithinAt (J n m) (J n (m + 1) x) I.interval x) (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ (n m : ℕ), ∀ x ∈ I.interval, |J n m x| ≤ C * w n m) (n : ℕ) {x : ℝ} (hx : x ∈ I.interval) : coefficient I w (ofJetFamily I w hw J hcont hderiv C hC hbound) n x = J n 0 x

theorem NavierStokes.AxisCoefficientSpace.norm_ofJetFamily_le (I : Window) (w : ℕ → ℕ → ℝ) (hw : ∀ (n m : ℕ), 0 < w n m) (J : ℕ → ℕ → ℝ → ℝ) (hcont : ∀ (n m : ℕ), ContinuousOn (J n m) I.interval) (hderiv : ∀ (n m : ℕ), ∀ x ∈ I.interval, HasDerivWithinAt (J n m) (J n (m + 1) x) I.interval x) (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ (n m : ℕ), ∀ x ∈ I.interval, |J n m x| ≤ C * w n m) : ‖ofJetFamily I w hw J hcont hderiv C hC hbound‖ ≤ C

theorem NavierStokes.AxisCoefficientSpace.hasDerivWithinAt_iterated_smooth (I : Window) (F : ℕ → ℝ → ℝ) (hF : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (F n) I.interval) (n m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : HasDerivWithinAt (iteratedDerivWithin m (F n) I.interval) (iteratedDerivWithin (m + 1) (F n) I.interval x) I.interval x

A smooth coefficient family's genuine iterated derivatives form the adjacent derivative chain required by ofJetFamily.

noncomputable def NavierStokes.AxisCoefficientSpace.ofSmoothFamily (I : Window) (w : ℕ → ℕ → ℝ) (hw : ∀ (n m : ℕ), 0 < w n m) (F : ℕ → ℝ → ℝ) (hF : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (F n) I.interval) (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ (n m : ℕ), ∀ x ∈ I.interval, |iteratedDerivWithin m (F n) I.interval x| ≤ C * w n m) : ↥(CoefficientSpace I w)

Reverse constructor from actual smooth coefficient functions with uniform bounds on all their parameter derivatives.

Equations

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

theorem NavierStokes.AxisCoefficientSpace.jet_ofSmoothFamily (I : Window) (w : ℕ → ℕ → ℝ) (hw : ∀ (n m : ℕ), 0 < w n m) (F : ℕ → ℝ → ℝ) (hF : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (F n) I.interval) (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ (n m : ℕ), ∀ x ∈ I.interval, |iteratedDerivWithin m (F n) I.interval x| ≤ C * w n m) (n m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : jet I w (↑(ofSmoothFamily I w hw F hF C hC hbound)) n m x = iteratedDerivWithin m (F n) I.interval x

theorem NavierStokes.AxisCoefficientSpace.coefficient_ofSmoothFamily (I : Window) (w : ℕ → ℕ → ℝ) (hw : ∀ (n m : ℕ), 0 < w n m) (F : ℕ → ℝ → ℝ) (hF : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (F n) I.interval) (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ (n m : ℕ), ∀ x ∈ I.interval, |iteratedDerivWithin m (F n) I.interval x| ≤ C * w n m) (n : ℕ) {x : ℝ} (hx : x ∈ I.interval) : coefficient I w (ofSmoothFamily I w hw F hF C hC hbound) n x = F n x

theorem NavierStokes.AxisCoefficientSpace.norm_ofSmoothFamily_le (I : Window) (w : ℕ → ℕ → ℝ) (hw : ∀ (n m : ℕ), 0 < w n m) (F : ℕ → ℝ → ℝ) (hF : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (F n) I.interval) (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ (n m : ℕ), ∀ x ∈ I.interval, |iteratedDerivWithin m (F n) I.interval x| ≤ C * w n m) : ‖ofSmoothFamily I w hw F hF C hC hbound‖ ≤ C

@[reducible, inline]

noncomputable abbrev NavierStokes.AxisCoefficientSpace.AxisSpace (I : Window) (ε : ℝ) : Submodule ℝ (RawJets I)

The specific space in GAX.2, with the manuscript's exact positive weights when ε>0. Completeness and normed vector-space structures are inherited.

Equations

• NavierStokes.AxisCoefficientSpace.AxisSpace I ε = NavierStokes.AxisCoefficientSpace.CoefficientSpace I (NavierStokes.AxisWeightEstimates.weight ε)

theorem NavierStokes.AxisCoefficientSpace.axisSpace_complete (I : Window) (ε : ℝ) : CompleteSpace ↥(AxisSpace I ε)

The concrete space is a complete normed space of actual smooth functions.

theorem NavierStokes.AxisCoefficientSpace.axisSpace_smooth (I : Window) (ε : ℝ) (A : ↥(AxisSpace I ε)) (n : ℕ) : ContDiffOn ℝ (↑⊤) (coefficient I (AxisWeightEstimates.weight ε) A n) I.interval

theorem NavierStokes.AxisCoefficientSpace.axisSpace_derivative_bound (I : Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisSpace I ε)) (n m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : |iteratedDerivWithin m (coefficient I (AxisWeightEstimates.weight ε) A n) I.interval x| ≤ AxisWeightEstimates.weight ε n m * ‖A‖

Each actual derivative is controlled by exactly the printed weight.

theorem NavierStokes.AxisCoefficientSpace.axisSpace_norm_le_iff (I : Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisSpace I ε)) (C : ℝ) (hC : 0 ≤ C) : ‖A‖ ≤ C ↔ ∀ (n m : ℕ) (x : ↑I.interval), |iteratedDerivWithin m (coefficient I (AxisWeightEstimates.weight ε) A n) I.interval ↑x| / AxisWeightEstimates.weight ε n m ≤ C

The exact manuscript norm, with actual derivatives in its quotient.