Actual shifted transport primitives

The source is integrated along a fixed translation direction. All integrals are Bochner integrals. Compact radial support is used to justify local fixed finite integration intervals, so ordinary derivatives pass under the integral without differentiating the translation parameter.

The translated radial integral and repeated integration by parts

The integrals and derivatives in this file are actual Bochner integrals and Fréchet derivatives. The auxiliary variable may be the universal cover of a torus. A separately constructed directional primitive supplies the inverse identity; no decay estimate for the integral is assumed.

def NavierStokes.RadialAlias.shift {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (M : ℝ) (v Y : E) (u : ℝ) : ℝ × E

The actual line along which the auxiliary variable is translated.

Equations

• NavierStokes.RadialAlias.shift M v Y u = (u, Y + (M * u) • v)

noncomputable def NavierStokes.RadialAlias.aliasIntegral {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (a b M : ℝ) (v Y : E) (f : ℝ × E → F) : F

The translated integral over the radial support interval.

Equations

• NavierStokes.RadialAlias.aliasIntegral a b M v Y f = ∫ (u : ℝ) in a..b, f (NavierStokes.RadialAlias.shift M v Y u)

noncomputable def NavierStokes.RadialAlias.wholeAlias {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (M : ℝ) (v Y : E) (f : ℝ × E → F) : F

The same integral over the whole radial line.

Equations

• NavierStokes.RadialAlias.wholeAlias M v Y f = ∫ (u : ℝ), f (NavierStokes.RadialAlias.shift M v Y u)

def NavierStokes.RadialAlias.RadiallySupported {E : Type u_1} {F : Type u_2} [NormedAddCommGroup F] (a b : ℝ) (f : ℝ × E → F) : Prop

Support in a fixed radial interval, uniformly in the auxiliary variable.

Equations

• NavierStokes.RadialAlias.RadiallySupported a b f = (Function.support f ⊆ Prod.fst ⁻¹' Set.Icc a b)

noncomputable def NavierStokes.RadialAlias.slowDeriv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : ℝ × E → F) (z : ℝ × E) : F

The derivative in the slow radial coordinate, holding the auxiliary variable fixed.

Equations

• NavierStokes.RadialAlias.slowDeriv f z = (fderiv ℝ f z) (1, 0)

noncomputable def NavierStokes.RadialAlias.directionalDeriv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (v : E) (f : ℝ × E → F) (z : ℝ × E) : F

The actual auxiliary directional derivative.

Equations

• NavierStokes.RadialAlias.directionalDeriv v f z = (fderiv ℝ f z) (0, v)

theorem NavierStokes.RadialAlias.shift_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (M : ℝ) (v Y : E) (u : ℝ) : HasDerivAt (shift M v Y) (1, M • v) u

theorem NavierStokes.RadialAlias.shift_continuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (M : ℝ) (v Y : E) : Continuous (shift M v Y)

theorem NavierStokes.RadialAlias.shifted_hasDerivAt {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {g : ℝ × E → F} {M u : ℝ} {v Y : E} (hg : DifferentiableAt ℝ g (shift M v Y u)) : HasDerivAt (fun (s : ℝ) => g (shift M v Y s)) (slowDeriv g (shift M v Y u) + M • directionalDeriv v g (shift M v Y u)) u

This is the chain rule d/du = ∂u + M L_v on the translated source.

theorem NavierStokes.RadialAlias.slowDeriv_continuous {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {g : ℝ × E → F} (hg : ContDiff ℝ 1 g) : Continuous (slowDeriv g)

theorem NavierStokes.RadialAlias.directionalDeriv_continuous {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {g : ℝ × E → F} (hg : ContDiff ℝ 1 g) (v : E) : Continuous (directionalDeriv v g)

theorem NavierStokes.RadialAlias.shifted_support_subset {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] {a b : ℝ} {g : ℝ × E → F} (hg : RadiallySupported a b g) (M : ℝ) (v Y : E) : (Function.support fun (u : ℝ) => g (shift M v Y u)) ⊆ Set.Icc a b

theorem NavierStokes.RadialAlias.radialSupport_fderiv_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} {g : ℝ × E → F} (hg : RadiallySupported a b g) (w : ℝ × E) : RadiallySupported a b fun (z : ℝ × E) => (fderiv ℝ g z) w

theorem NavierStokes.RadialAlias.radialSupport_slowDeriv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} {g : ℝ × E → F} (hg : RadiallySupported a b g) : RadiallySupported a b (slowDeriv g)

theorem NavierStokes.RadialAlias.radialSupport_directionalDeriv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} {g : ℝ × E → F} (hg : RadiallySupported a b g) (v : E) : RadiallySupported a b (directionalDeriv v g)

theorem NavierStokes.RadialAlias.endpoint_zero_of_support {F : Type u_2} [NormedAddCommGroup F] {a b : ℝ} {g : ℝ → F} (hc : Continuous g) (hs : Function.support g ⊆ Set.Icc a b) : g a = 0 ∧ g b = 0

theorem NavierStokes.RadialAlias.aliasIntegral_eq_wholeAlias {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v Y : E} {g : ℝ × E → F} (hc : Continuous g) (hs : RadiallySupported a b g) : aliasIntegral a b M v Y g = wholeAlias M v Y g

Compact radial support makes the finite interval integral the whole-line integral.

theorem NavierStokes.RadialAlias.aliasIntegral_directionalDeriv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b M : ℝ} {v Y : E} {g : ℝ × E → F} (hM : M ≠ 0) (hg : ContDiff ℝ 1 g) (hs : RadiallySupported a b g) : aliasIntegral a b M v Y (directionalDeriv v g) = -M⁻¹ • aliasIntegral a b M v Y (slowDeriv g)

One integration by parts, including the minus sign and the inverse factor.

theorem NavierStokes.RadialAlias.wholeAlias_directionalDeriv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b M : ℝ} {v Y : E} {g : ℝ × E → F} (hM : M ≠ 0) (hg : ContDiff ℝ 1 g) (hs : RadiallySupported a b g) : wholeAlias M v Y (directionalDeriv v g) = -M⁻¹ • wholeAlias M v Y (slowDeriv g)

noncomputable def NavierStokes.RadialAlias.sourceJet {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (J : (ℝ × E → F) → ℝ × E → F) (f : ℝ × E → F) (p : ℕ) : ℝ × E → F

Successive actual slow derivatives of directional primitives.

Equations

• NavierStokes.RadialAlias.sourceJet J f p = (NavierStokes.RadialAlias.slowDeriv ∘ J)^[p] f

@[simp]

theorem NavierStokes.RadialAlias.sourceJet_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (J : (ℝ × E → F) → ℝ × E → F) (f : ℝ × E → F) : sourceJet J f 0 = f

theorem NavierStokes.RadialAlias.sourceJet_succ {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (J : (ℝ × E → F) → ℝ × E → F) (f : ℝ × E → F) (p : ℕ) : sourceJet J f (p + 1) = slowDeriv (J (sourceJet J f p))

theorem NavierStokes.RadialAlias.sourceJet_eq_deriv_inverse_iterate {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (J : (ℝ × E → F) → ℝ × E → F) (f : ℝ × E → F) (p : ℕ) (hcomm : Function.Commute slowDeriv J) : sourceJet J f p = slowDeriv^[p] (J^[p] f)

When the inverse commutes with slow differentiation, these are literally ∂u^p (J^p f), as in the manuscript.

theorem NavierStokes.RadialAlias.wholeAlias_sourceJet {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b M : ℝ} {v Y : E} (J : (ℝ × E → F) → ℝ × E → F) (f : ℝ × E → F) (p : ℕ) (hM : M ≠ 0) (hJ : ∀ n < p, ContDiff ℝ 1 (J (sourceJet J f n))) (hs : ∀ n < p, RadiallySupported a b (J (sourceJet J f n))) (hr : ∀ n < p, directionalDeriv v (J (sourceJet J f n)) = sourceJet J f n) : wholeAlias M v Y f = (-M⁻¹) ^ p • wholeAlias M v Y (sourceJet J f p)

Arbitrarily many integrations by parts. The hypotheses concern actual directional derivatives, smoothness and support; no integral estimate is assumed.

theorem NavierStokes.RadialAlias.wholeAlias_inverse_iterate {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b M : ℝ} {v Y : E} (J : (ℝ × E → F) → ℝ × E → F) (f : ℝ × E → F) (p : ℕ) (hM : M ≠ 0) (hcomm : Function.Commute slowDeriv J) (hJ : ∀ n < p, ContDiff ℝ 1 (J (sourceJet J f n))) (hs : ∀ n < p, RadiallySupported a b (J (sourceJet J f n))) (hr : ∀ n < p, directionalDeriv v (J (sourceJet J f n)) = sourceJet J f n) : wholeAlias M v Y f = (-M⁻¹) ^ p • wholeAlias M v Y (slowDeriv^[p] (J^[p] f))

The manuscript's literal ∂u^p J^p form, with the sign displayed.

theorem NavierStokes.RadialAlias.sourceJet_continuous {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (J : (ℝ × E → F) → ℝ × E → F) (f : ℝ × E → F) (p : ℕ) (hf : Continuous f) (hJ : ∀ n < p, ContDiff ℝ 1 (J (sourceJet J f n))) : Continuous (sourceJet J f p)

theorem NavierStokes.RadialAlias.sourceJet_radiallySupported {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} (J : (ℝ × E → F) → ℝ × E → F) (f : ℝ × E → F) (p : ℕ) (hf : RadiallySupported a b f) (hs : ∀ n < p, RadiallySupported a b (J (sourceJet J f n))) : RadiallySupported a b (sourceJet J f p)

theorem NavierStokes.RadialAlias.wholeAlias_norm_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M C : ℝ} {v Y : E} {f : ℝ × E → F} (hab : a ≤ b) (hf : Continuous f) (hs : RadiallySupported a b f) (hbound : ∀ u ∈ Set.Icc a b, ∀ (Z : E), ‖f (u, Z)‖ ≤ C) : ‖wholeAlias M v Y f‖ ≤ C * |b - a|

theorem NavierStokes.RadialAlias.wholeAlias_sourceJet_norm_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b M C : ℝ} {v Y : E} (J : (ℝ × E → F) → ℝ × E → F) (f : ℝ × E → F) (p : ℕ) (hab : a ≤ b) (hM : M ≠ 0) (hf : Continuous f) (hfs : RadiallySupported a b f) (hJ : ∀ n < p, ContDiff ℝ 1 (J (sourceJet J f n))) (hs : ∀ n < p, RadiallySupported a b (J (sourceJet J f n))) (hr : ∀ n < p, directionalDeriv v (J (sourceJet J f n)) = sourceJet J f n) (hbound : ∀ u ∈ Set.Icc a b, ∀ (Z : E), ‖sourceJet J f p (u, Z)‖ ≤ C) : ‖wholeAlias M v Y f‖ ≤ |M|⁻¹ ^ p * (C * |b - a|)

The all-order gain has a constant uniform in the translation parameter Y and in M whenever the last source-jet bound is uniform.

theorem NavierStokes.TransportPrimitive.uniform_local_bound {H G : Type u} [NormedAddCommGroup H] [NormedAddCommGroup G] {g : H × ℝ → G} (hg : Continuous g) (x : H) (a b : ℝ) : ∃ ε > 0, ∃ (C : ℝ), ∀ y ∈ Metric.ball x ε, ∀ u ∈ Set.uIcc a b, ‖g (y, u)‖ ≤ C

Continuity gives a uniform bound near a parameter value on a compact interval. The parameter space need not be finite dimensional.

noncomputable def NavierStokes.TransportPrimitive.parameterDerivative {H G : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup G] [NormedSpace ℝ G] (g : H × ℝ → G) (z : H × ℝ) : H →L[ℝ] G

The parameter derivative of a jointly smooth integrand.

Equations

• NavierStokes.TransportPrimitive.parameterDerivative g z = fderiv ℝ g z ∘SL ContinuousLinearMap.inl ℝ H ℝ

theorem NavierStokes.TransportPrimitive.parameterDerivative_contDiff {H G : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup G] [NormedSpace ℝ G] {g : H × ℝ → G} (hg : ContDiff ℝ (↑⊤) g) : ContDiff ℝ (↑⊤) (parameterDerivative g)

theorem NavierStokes.TransportPrimitive.parameter_hasFDerivAt {H G : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup G] [NormedSpace ℝ G] {g : H × ℝ → G} (hg : ContDiff ℝ (↑⊤) g) (x : H) (u : ℝ) : HasFDerivAt (fun (y : H) => g (y, u)) (parameterDerivative g (x, u)) x

theorem NavierStokes.TransportPrimitive.parameterIntegral_hasFDerivAt {H G : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup G] [NormedSpace ℝ G] {g : H × ℝ → G} (hg : ContDiff ℝ (↑⊤) g) (a b : ℝ) (x : H) : HasFDerivAt (fun (y : H) => ∫ (u : ℝ) in a..b, g (y, u)) (∫ (u : ℝ) in a..b, parameterDerivative g (x, u)) x

theorem NavierStokes.TransportPrimitive.parameterIntegral_contDiff_nat {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] (n : ℕ) {G : Type u} [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace G] {g : H × ℝ → G} : ContDiff ℝ (↑⊤) g → ∀ (a b : ℝ), ContDiff ℝ ↑↑n fun (y : H) => ∫ (u : ℝ) in a..b, g (y, u)

Smoothness of a genuine integral over a fixed finite interval, with arbitrary normed parameter space and Banach-valued output.

theorem NavierStokes.TransportPrimitive.parameterIntegral_contDiff {H G : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace G] {g : H × ℝ → G} (hg : ContDiff ℝ (↑⊤) g) (a b : ℝ) : ContDiff ℝ ↑⊤ fun (y : H) => ∫ (u : ℝ) in a..b, g (y, u)

noncomputable def NavierStokes.TransportPrimitive.shift {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (M : ℝ) (v : E) (z : ℝ × E) (u : ℝ) : ℝ × E

A fixed translation along the transport direction.

Equations

• NavierStokes.TransportPrimitive.shift M v z u = z + (u, (M * u) • v)

noncomputable def NavierStokes.TransportPrimitive.pastIntegral {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (M : ℝ) (v : E) (f : ℝ × E → F) (z : ℝ × E) : F

The past half-line primitive, in fixed integration coordinates.

Equations

• NavierStokes.TransportPrimitive.pastIntegral M v f z = ∫ (u : ℝ) in Set.Iic 0, f (NavierStokes.TransportPrimitive.shift M v z u)

noncomputable def NavierStokes.TransportPrimitive.totalIntegral {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (M : ℝ) (v : E) (f : ℝ × E → F) (z : ℝ × E) : F

The complete translated radial integral.

Equations

• NavierStokes.TransportPrimitive.totalIntegral M v f z = ∫ (u : ℝ), f (NavierStokes.TransportPrimitive.shift M v z u)

noncomputable def NavierStokes.TransportPrimitive.compactIntegral {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (χ : ℝ → ℝ) (M : ℝ) (v : E) (f : ℝ × E → F) (z : ℝ × E) : F

Compactification with a fixed radial cutoff.

Equations

• NavierStokes.TransportPrimitive.compactIntegral χ M v f z = NavierStokes.TransportPrimitive.pastIntegral M v f z - χ z.1 • NavierStokes.TransportPrimitive.totalIntegral M v f z

@[simp]

theorem NavierStokes.TransportPrimitive.shift_fst {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (M : ℝ) (v : E) (z : ℝ × E) (u : ℝ) : (shift M v z u).1 = z.1 + u

@[simp]

theorem NavierStokes.TransportPrimitive.shift_snd {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (M : ℝ) (v : E) (z : ℝ × E) (u : ℝ) : (shift M v z u).2 = z.2 + (M * u) • v

@[simp]

theorem NavierStokes.TransportPrimitive.shift_zero {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (M : ℝ) (v : E) (z : ℝ × E) : shift M v z 0 = z

theorem NavierStokes.TransportPrimitive.shift_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (M : ℝ) (v : E) : ContDiff ℝ ↑⊤ fun (p : (ℝ × E) × ℝ) => shift M v p.1 p.2

theorem NavierStokes.TransportPrimitive.shifted_continuous {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] {f : ℝ × E → F} (hf : Continuous f) (M : ℝ) (v : E) (z : ℝ × E) : Continuous fun (u : ℝ) => f (shift M v z u)

theorem NavierStokes.TransportPrimitive.shifted_support_subset {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hs : RadialAlias.RadiallySupported a b f) (z : ℝ × E) : (Function.support fun (u : ℝ) => f (shift M v z u)) ⊆ Set.Icc (a - z.1) (b - z.1)

theorem NavierStokes.TransportPrimitive.shifted_integrable {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hf : Continuous f) (hs : RadialAlias.RadiallySupported a b f) (z : ℝ × E) : MeasureTheory.Integrable (fun (u : ℝ) => f (shift M v z u)) MeasureTheory.volume

theorem NavierStokes.TransportPrimitive.radial_zero_of_lt {E F : Type} [NormedAddCommGroup F] {a b : ℝ} {f : ℝ × E → F} (hs : RadialAlias.RadiallySupported a b f) {z : ℝ × E} (hz : z.1 < a) : f z = 0

theorem NavierStokes.TransportPrimitive.radial_zero_of_gt {E F : Type} [NormedAddCommGroup F] {a b : ℝ} {f : ℝ × E → F} (hs : RadialAlias.RadiallySupported a b f) {z : ℝ × E} (hz : b < z.1) : f z = 0

theorem NavierStokes.TransportPrimitive.pastIntegral_eq_interval {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M c : ℝ} {v : E} {f : ℝ × E → F} (hf : Continuous f) (hs : RadialAlias.RadiallySupported a b f) (z : ℝ × E) (hc : z.1 + c < a) : pastIntegral M v f z = ∫ (u : ℝ) in c..0, f (shift M v z u)

The past integral is locally a finite interval integral with fixed endpoints.

theorem NavierStokes.TransportPrimitive.totalIntegral_eq_interval {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M c d : ℝ} {v : E} {f : ℝ × E → F} (hs : RadialAlias.RadiallySupported a b f) (z : ℝ × E) (hc : z.1 + c < a) (hd : b ≤ z.1 + d) : totalIntegral M v f z = ∫ (u : ℝ) in c..d, f (shift M v z u)

theorem NavierStokes.TransportPrimitive.pastIntegral_eventually_eq_interval {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hf : Continuous f) (hs : RadialAlias.RadiallySupported a b f) (z : ℝ × E) : pastIntegral M v f =ᶠ[nhds z] fun (y : ℝ × E) => ∫ (u : ℝ) in a - z.1 - 1..0, f (shift M v y u)

theorem NavierStokes.TransportPrimitive.totalIntegral_eventually_eq_interval {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hs : RadialAlias.RadiallySupported a b f) (z : ℝ × E) : totalIntegral M v f =ᶠ[nhds z] fun (y : ℝ × E) => ∫ (u : ℝ) in a - z.1 - 1..b - z.1 + 1, f (shift M v y u)

theorem NavierStokes.TransportPrimitive.pastIntegral_contDiff {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) : ContDiff ℝ (↑⊤) (pastIntegral M v f)

theorem NavierStokes.TransportPrimitive.totalIntegral_contDiff {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) : ContDiff ℝ (↑⊤) (totalIntegral M v f)

theorem NavierStokes.TransportPrimitive.compactIntegral_contDiff {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b M : ℝ} {v : E} {f : ℝ × E → F} {χ : ℝ → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) : ContDiff ℝ (↑⊤) (compactIntegral χ M v f)

theorem NavierStokes.TransportPrimitive.radialSupport_fderiv {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} {f : ℝ × E → F} (hs : RadialAlias.RadiallySupported a b f) : RadialAlias.RadiallySupported a b (fderiv ℝ f)

All actual Fréchet derivatives retain radial support.

theorem NavierStokes.TransportPrimitive.parameterDerivative_shifted {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ × E → F} (hf : ContDiff ℝ (↑⊤) f) (M : ℝ) (v : E) (z : ℝ × E) (u : ℝ) : parameterDerivative (fun (p : (ℝ × E) × ℝ) => f (shift M v p.1 p.2)) (z, u) = fderiv ℝ f (shift M v z u)

theorem NavierStokes.TransportPrimitive.pastIntegral_hasFDerivAt {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (z : ℝ × E) : HasFDerivAt (pastIntegral M v f) (pastIntegral M v (fderiv ℝ f) z) z

The entire Fréchet derivative commutes with the fixed-u past integral.

theorem NavierStokes.TransportPrimitive.totalIntegral_hasFDerivAt {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (z : ℝ × E) : HasFDerivAt (totalIntegral M v f) (totalIntegral M v (fderiv ℝ f) z) z

noncomputable def NavierStokes.TransportPrimitive.fixedDeriv {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (w : ℝ × E) (f : ℝ × E → F) (z : ℝ × E) : F

An ordinary derivative in any fixed direction, including a slow parameter.

Equations

• NavierStokes.TransportPrimitive.fixedDeriv w f z = (fderiv ℝ f z) w

theorem NavierStokes.TransportPrimitive.fixedDeriv_contDiff {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ × E → F} (hf : ContDiff ℝ (↑⊤) f) (w : ℝ × E) : ContDiff ℝ (↑⊤) (fixedDeriv w f)

theorem NavierStokes.TransportPrimitive.fixedDeriv_supported {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} {f : ℝ × E → F} (hs : RadialAlias.RadiallySupported a b f) (w : ℝ × E) : RadialAlias.RadiallySupported a b (fixedDeriv w f)

theorem NavierStokes.TransportPrimitive.fixedDeriv_pastIntegral {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (w z : ℝ × E) : fixedDeriv w (pastIntegral M v f) z = pastIntegral M v (fixedDeriv w f) z

theorem NavierStokes.TransportPrimitive.fixedDeriv_totalIntegral {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (w z : ℝ × E) : fixedDeriv w (totalIntegral M v f) z = totalIntegral M v (fixedDeriv w f) z

theorem NavierStokes.TransportPrimitive.shift_hasDerivAt {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (M : ℝ) (v : E) (z : ℝ × E) (u : ℝ) : HasDerivAt (shift M v z) (1, M • v) u

theorem NavierStokes.TransportPrimitive.shifted_hasDerivAt {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ × E → F} (hf : ContDiff ℝ (↑⊤) f) (M : ℝ) (v : E) (z : ℝ × E) (u : ℝ) : HasDerivAt (fun (t : ℝ) => f (shift M v z t)) (fixedDeriv (1, M • v) f (shift M v z u)) u

theorem NavierStokes.TransportPrimitive.transport_pastIntegral {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (z : ℝ × E) : fixedDeriv (1, M • v) (pastIntegral M v f) z = f z

The exact transport identity, proved by the fundamental theorem of calculus.

theorem NavierStokes.TransportPrimitive.transport_totalIntegral {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (z : ℝ × E) : fixedDeriv (1, M • v) (totalIntegral M v f) z = 0

The complete translated integral is constant along each transport line.

theorem NavierStokes.TransportPrimitive.transport_eq_partials {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (M : ℝ) (v : E) (f : ℝ × E → F) (z : ℝ × E) : fixedDeriv (1, M • v) f z = fixedDeriv (1, 0) f z + M • fixedDeriv (0, v) f z

This derivative is exactly ∂U + M v·∂Y.

theorem NavierStokes.TransportPrimitive.fixedDeriv_compactIntegral {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f : ℝ × E → F} {χ : ℝ → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (w z : ℝ × E) : fixedDeriv w (compactIntegral χ M v f) z = compactIntegral χ M v (fixedDeriv w f) z - (deriv χ z.1 * w.1) • totalIntegral M v f z

The cutoff product rule retains the actual ordinary radial derivative.

theorem NavierStokes.TransportPrimitive.transport_compactIntegral {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b M : ℝ} {v : E} {f : ℝ × E → F} {χ : ℝ → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (z : ℝ × E) : fixedDeriv (1, M • v) (compactIntegral χ M v f) z = f z - deriv χ z.1 • totalIntegral M v f z

theorem NavierStokes.TransportPrimitive.auxiliaryDeriv_compactIntegral {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f : ℝ × E → F} {χ : ℝ → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (w : E) (z : ℝ × E) : fixedDeriv (0, w) (compactIntegral χ M v f) z = compactIntegral χ M v (fixedDeriv (0, w) f) z

theorem NavierStokes.TransportPrimitive.radial_zero_of_le {E F : Type} [NormedAddCommGroup E] [NormedAddCommGroup F] {a b : ℝ} {f : ℝ × E → F} (hf : Continuous f) (hs : RadialAlias.RadiallySupported a b f) {z : ℝ × E} (hz : z.1 ≤ a) : f z = 0

theorem NavierStokes.TransportPrimitive.pastIntegral_eq_zero_of_le {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hf : Continuous f) (hs : RadialAlias.RadiallySupported a b f) (z : ℝ × E) (hz : z.1 ≤ a) : pastIntegral M v f z = 0

theorem NavierStokes.TransportPrimitive.pastIntegral_eq_total_of_ge {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hs : RadialAlias.RadiallySupported a b f) (z : ℝ × E) (hz : b ≤ z.1) : pastIntegral M v f z = totalIntegral M v f z

theorem NavierStokes.TransportPrimitive.compactIntegral_supported {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f : ℝ × E → F} {χ : ℝ → ℝ} (hf : Continuous f) (hs : RadialAlias.RadiallySupported a b f) (hleft : ∀ u ≤ a, χ u = 0) (hright : ∀ (u : ℝ), b ≤ u → χ u = 1) : RadialAlias.RadiallySupported a b (compactIntegral χ M v f)

noncomputable def NavierStokes.TransportPrimitive.cutoff (c d u : ℝ) : ℝ

An explicit smooth transition with specified plateau thresholds.

Equations

• NavierStokes.TransportPrimitive.cutoff c d u = ((u - c) / (d - c)).smoothTransition

theorem NavierStokes.TransportPrimitive.cutoff_contDiff (c d : ℝ) : ContDiff ℝ (↑⊤) (cutoff c d)

theorem NavierStokes.TransportPrimitive.cutoff_zero {c d u : ℝ} (hcd : c < d) (hu : u ≤ c) : cutoff c d u = 0

theorem NavierStokes.TransportPrimitive.cutoff_one {c d u : ℝ} (hcd : c < d) (hu : d ≤ u) : cutoff c d u = 1

theorem NavierStokes.TransportPrimitive.cutoff_mem_Icc (c d u : ℝ) : cutoff c d u ∈ Set.Icc 0 1

noncomputable def NavierStokes.TransportPrimitive.interiorCutoff (a b : ℝ) : ℝ → ℝ

The canonical cutoff has both plateaus strictly inside the support interval.

Equations

• NavierStokes.TransportPrimitive.interiorCutoff a b = NavierStokes.TransportPrimitive.cutoff ((2 * a + b) / 3) ((a + 2 * b) / 3)

theorem NavierStokes.TransportPrimitive.interiorCutoff_contDiff (a b : ℝ) : ContDiff ℝ (↑⊤) (interiorCutoff a b)

theorem NavierStokes.TransportPrimitive.interiorCutoff_zero {a b u : ℝ} (hab : a < b) (hu : u ≤ (2 * a + b) / 3) : interiorCutoff a b u = 0

theorem NavierStokes.TransportPrimitive.interiorCutoff_one {a b u : ℝ} (hab : a < b) (hu : (a + 2 * b) / 3 ≤ u) : interiorCutoff a b u = 1

theorem NavierStokes.TransportPrimitive.canonicalCompact_supported {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hab : a < b) (hf : Continuous f) (hs : RadialAlias.RadiallySupported a b f) : RadialAlias.RadiallySupported a b (compactIntegral (interiorCutoff a b) M v f)

noncomputable def NavierStokes.TransportPrimitive.futureIntegral {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (M : ℝ) (v : E) (f : ℝ × E → F) (z : ℝ × E) : F

The complementary future integral used at the right support edge.

Equations

• NavierStokes.TransportPrimitive.futureIntegral M v f z = ∫ (u : ℝ) in Set.Ioi 0, f (NavierStokes.TransportPrimitive.shift M v z u)

theorem NavierStokes.TransportPrimitive.past_add_future {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hf : Continuous f) (hs : RadialAlias.RadiallySupported a b f) (z : ℝ × E) : pastIntegral M v f z + futureIntegral M v f z = totalIntegral M v f z

theorem NavierStokes.TransportPrimitive.compactIntegral_eq_neg_future {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f : ℝ × E → F} {χ : ℝ → ℝ} (hf : Continuous f) (hs : RadialAlias.RadiallySupported a b f) (z : ℝ × E) (hχ : χ z.1 = 1) : compactIntegral χ M v f z = -futureIntegral M v f z

theorem NavierStokes.TransportPrimitive.pastIntegral_eq_supportInterval {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hf : Continuous f) (hs : RadialAlias.RadiallySupported a b f) (z : ℝ × E) : pastIntegral M v f z = ∫ (u : ℝ) in a - z.1..0, f (shift M v z u)

theorem NavierStokes.TransportPrimitive.totalIntegral_eq_supportInterval {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hf : Continuous f) (hs : RadialAlias.RadiallySupported a b f) (z : ℝ × E) : totalIntegral M v f z = ∫ (u : ℝ) in a - z.1..b - z.1, f (shift M v z u)

theorem NavierStokes.TransportPrimitive.pastIntegral_eq_radialInterval {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hf : Continuous f) (hs : RadialAlias.RadiallySupported a b f) (z : ℝ × E) : pastIntegral M v f z = ∫ (s : ℝ) in a..z.1, f (s, z.2 + (M * (s - z.1)) • v)

The alternative radial-coordinate formula is derived by translation.

theorem NavierStokes.TransportPrimitive.totalIntegral_eq_radialInterval {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hf : Continuous f) (hs : RadialAlias.RadiallySupported a b f) (z : ℝ × E) : totalIntegral M v f z = ∫ (s : ℝ) in a..b, f (s, z.2 + (M * (s - z.1)) • v)

theorem NavierStokes.TransportPrimitive.futureIntegral_eq_radialInterval {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hf : Continuous f) (hs : RadialAlias.RadiallySupported a b f) (z : ℝ × E) : futureIntegral M v f z = ∫ (s : ℝ) in z.1..b, f (s, z.2 + (M * (s - z.1)) • v)

theorem NavierStokes.TransportPrimitive.totalIntegral_norm_le {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M C : ℝ} {v : E} {f : ℝ × E → F} (hab : a ≤ b) (hf : Continuous f) (hs : RadialAlias.RadiallySupported a b f) (hbound : ∀ s ∈ Set.Icc a b, ∀ (Y : E), ‖f (s, Y)‖ ≤ C) (z : ℝ × E) : ‖totalIntegral M v f z‖ ≤ C * (b - a)

theorem NavierStokes.TransportPrimitive.pastIntegral_norm_le {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M C : ℝ} {v : E} {f : ℝ × E → F} (hab : a ≤ b) (hf : Continuous f) (hs : RadialAlias.RadiallySupported a b f) (hbound : ∀ s ∈ Set.Icc a b, ∀ (Y : E), ‖f (s, Y)‖ ≤ C) (z : ℝ × E) : ‖pastIntegral M v f z‖ ≤ C * (b - a)

Only the radial support length enters; there is no power of M in this bound.

theorem NavierStokes.TransportPrimitive.compactIntegral_norm_le {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M C K : ℝ} {v : E} {f : ℝ × E → F} {χ : ℝ → ℝ} (hab : a ≤ b) (hf : Continuous f) (hs : RadialAlias.RadiallySupported a b f) (hbound : ∀ s ∈ Set.Icc a b, ∀ (Y : E), ‖f (s, Y)‖ ≤ C) (hK : 0 ≤ K) (hχ : ∀ (u : ℝ), |χ u| ≤ K) (z : ℝ × E) : ‖compactIntegral χ M v f z‖ ≤ (1 + K) * C * (b - a)

theorem NavierStokes.TransportPrimitive.pastIntegral_add {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f g : ℝ × E → F} (hf : Continuous f) (hg : Continuous g) (hsf : RadialAlias.RadiallySupported a b f) (hsg : RadialAlias.RadiallySupported a b g) (z : ℝ × E) : pastIntegral M v (fun (x : ℝ × E) => f x + g x) z = pastIntegral M v f z + pastIntegral M v g z

theorem NavierStokes.TransportPrimitive.totalIntegral_add {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f g : ℝ × E → F} (hf : Continuous f) (hg : Continuous g) (hsf : RadialAlias.RadiallySupported a b f) (hsg : RadialAlias.RadiallySupported a b g) (z : ℝ × E) : totalIntegral M v (fun (x : ℝ × E) => f x + g x) z = totalIntegral M v f z + totalIntegral M v g z

theorem NavierStokes.TransportPrimitive.compactIntegral_add {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f g : ℝ × E → F} (hf : Continuous f) (hg : Continuous g) (hsf : RadialAlias.RadiallySupported a b f) (hsg : RadialAlias.RadiallySupported a b g) (χ : ℝ → ℝ) (z : ℝ × E) : compactIntegral χ M v (fun (x : ℝ × E) => f x + g x) z = compactIntegral χ M v f z + compactIntegral χ M v g z

theorem NavierStokes.TransportPrimitive.pastIntegral_smul {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (M c : ℝ) (v : E) (f : ℝ × E → F) (z : ℝ × E) : pastIntegral M v (fun (x : ℝ × E) => c • f x) z = c • pastIntegral M v f z

theorem NavierStokes.TransportPrimitive.totalIntegral_smul {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (M c : ℝ) (v : E) (f : ℝ × E → F) (z : ℝ × E) : totalIntegral M v (fun (x : ℝ × E) => c • f x) z = c • totalIntegral M v f z

theorem NavierStokes.TransportPrimitive.compactIntegral_smul {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (χ : ℝ → ℝ) (M c : ℝ) (v : E) (f : ℝ × E → F) (z : ℝ × E) : compactIntegral χ M v (fun (x : ℝ × E) => c • f x) z = c • compactIntegral χ M v f z

theorem NavierStokes.TransportPrimitive.iteratedFDeriv_supported {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} {f : ℝ × E → F} (hs : RadialAlias.RadiallySupported a b f) (n : ℕ) : RadialAlias.RadiallySupported a b (iteratedFDeriv ℝ n f)

theorem NavierStokes.TransportPrimitive.iteratedFDeriv_contDiff {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ × E → F} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) : ContDiff ℝ (↑⊤) (iteratedFDeriv ℝ n f)

theorem NavierStokes.TransportPrimitive.iteratedFDeriv_pastIntegral {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (n : ℕ) (z : ℝ × E) : iteratedFDeriv ℝ n (pastIntegral M v f) z = pastIntegral M v (iteratedFDeriv ℝ n f) z

Every order of the actual multilinear Fréchet derivative commutes with I.

theorem NavierStokes.TransportPrimitive.iteratedFDeriv_totalIntegral {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (n : ℕ) (z : ℝ × E) : iteratedFDeriv ℝ n (totalIntegral M v f) z = totalIntegral M v (iteratedFDeriv ℝ n f) z

Every order of the actual multilinear Fréchet derivative commutes with J.

theorem NavierStokes.TransportPrimitive.iteratedFDeriv_pastIntegral_norm_le {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M C : ℝ} {v : E} {f : ℝ × E → F} (hab : a ≤ b) (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (n : ℕ) (hbound : ∀ s ∈ Set.Icc a b, ∀ (Y : E), ‖iteratedFDeriv ℝ n f (s, Y)‖ ≤ C) (z : ℝ × E) : ‖iteratedFDeriv ℝ n (pastIntegral M v f) z‖ ≤ C * (b - a)

theorem NavierStokes.TransportPrimitive.iteratedFDeriv_totalIntegral_norm_le {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M C : ℝ} {v : E} {f : ℝ × E → F} (hab : a ≤ b) (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (n : ℕ) (hbound : ∀ s ∈ Set.Icc a b, ∀ (Y : E), ‖iteratedFDeriv ℝ n f (s, Y)‖ ≤ C) (z : ℝ × E) : ‖iteratedFDeriv ℝ n (totalIntegral M v f) z‖ ≤ C * (b - a)

theorem NavierStokes.TransportPrimitive.iteratedFDeriv_compactIntegral_eq {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b M : ℝ} {v : E} {f : ℝ × E → F} {χ : ℝ → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (n : ℕ) (z : ℝ × E) : iteratedFDeriv ℝ n (compactIntegral χ M v f) z = iteratedFDeriv ℝ n (pastIntegral M v f) z - iteratedFDeriv ℝ n (fun (y : ℝ × E) => χ y.1 • totalIntegral M v f y) z

theorem NavierStokes.TransportPrimitive.iteratedFDeriv_compactIntegral_norm_le {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b M : ℝ} {v : E} {f : ℝ × E → F} {χ : ℝ → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (n : ℕ) (z : ℝ × E) : ‖iteratedFDeriv ℝ n (compactIntegral χ M v f) z‖ ≤ ‖pastIntegral M v (iteratedFDeriv ℝ n f) z‖ + ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv ℝ i (fun (y : ℝ × E) => χ y.1) z‖ * ‖totalIntegral M v (iteratedFDeriv ℝ (n - i) f) z‖

Full binomial Leibniz bound. Every derivative of the cutoff is retained.

theorem NavierStokes.TransportPrimitive.iteratedFDeriv_compactIntegral_uniform {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b M : ℝ} {v : E} {f : ℝ × E → F} {χ : ℝ → ℝ} (hab : a ≤ b) (hχ : ContDiff ℝ (↑⊤) χ) (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (n : ℕ) (A B : ℕ → ℝ) (hB : ∀ i ≤ n, 0 ≤ B i) (hsource : ∀ j ≤ n, ∀ s ∈ Set.Icc a b, ∀ (Y : E), ‖iteratedFDeriv ℝ j f (s, Y)‖ ≤ A j) (hcutoff : ∀ i ≤ n, ∀ (z : ℝ × E), ‖iteratedFDeriv ℝ i (fun (y : ℝ × E) => χ y.1) z‖ ≤ B i) (z : ℝ × E) : ‖iteratedFDeriv ℝ n (compactIntegral χ M v f) z‖ ≤ (A n + ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * B i * A (n - i)) * (b - a)

Uniform all-order operator-norm estimate from a finite list of genuine source and cutoff derivative bounds. The constant contains no translation parameter.

theorem NavierStokes.TransportPrimitive.futureIntegral_eq_total_sub_past {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hf : Continuous f) (hs : RadialAlias.RadiallySupported a b f) (z : ℝ × E) : futureIntegral M v f z = totalIntegral M v f z - pastIntegral M v f z

theorem NavierStokes.TransportPrimitive.futureIntegral_contDiff {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) : ContDiff ℝ (↑⊤) (futureIntegral M v f)

theorem NavierStokes.TransportPrimitive.iteratedFDeriv_sub_of_smooth {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f g : ℝ × E → F} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (n : ℕ) (z : ℝ × E) : iteratedFDeriv ℝ n (fun (y : ℝ × E) => f y - g y) z = iteratedFDeriv ℝ n f z - iteratedFDeriv ℝ n g z

theorem NavierStokes.TransportPrimitive.iteratedFDeriv_futureIntegral {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (n : ℕ) (z : ℝ × E) : iteratedFDeriv ℝ n (futureIntegral M v f) z = futureIntegral M v (iteratedFDeriv ℝ n f) z

The future primitive has the same derivative commutation as the past primitive.

theorem NavierStokes.TransportPrimitive.futureIntegral_norm_le {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M C : ℝ} {v : E} {f : ℝ × E → F} (hab : a ≤ b) (hf : Continuous f) (hs : RadialAlias.RadiallySupported a b f) (hbound : ∀ s ∈ Set.Icc a b, ∀ (Y : E), ‖f (s, Y)‖ ≤ C) (z : ℝ × E) : ‖futureIntegral M v f z‖ ≤ C * (b - a)

theorem NavierStokes.TransportPrimitive.iteratedFDeriv_futureIntegral_norm_le {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b M C : ℝ} {v : E} {f : ℝ × E → F} (hab : a ≤ b) (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (n : ℕ) (hbound : ∀ s ∈ Set.Icc a b, ∀ (Y : E), ‖iteratedFDeriv ℝ n f (s, Y)‖ ≤ C) (z : ℝ × E) : ‖iteratedFDeriv ℝ n (futureIntegral M v f) z‖ ≤ C * (b - a)

theorem NavierStokes.TransportPrimitive.totalIntegral_eq_wholeAlias {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {f : ℝ × E → F} (hf : Continuous f) (hs : RadialAlias.RadiallySupported a b f) (z : ℝ × E) : totalIntegral M v f z = RadialAlias.wholeAlias M v (z.2 - (M * z.1) • v) f

The total integral agrees with the separately formalized radial alias.