Joint dependence of terminal flat primitive factors

The coefficient depends on a finite-dimensional auxiliary parameter and the edge coordinate. The factor is the actual transformed improper integral.

theorem NavierStokes.ParametricFlatFactor.contDiffAt_partial_iteratedFDeriv {P : Type u_1} {Y : Type u_2} {Z : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [NormedAddCommGroup Z] [NormedSpace ℝ Z] (F : P → Y → Z) (n : ℕ) (p : P) (y : Y) (hF : ContDiffAt ℝ (↑⊤) (Function.uncurry F) (p, y)) : ContDiffAt ℝ (↑⊤) (fun (z : P × Y) => iteratedFDeriv ℝ n (F z.1) z.2) (p, y)

Actual iterated partial derivatives retain local joint smoothness. The proof uses the derivative recursion, not independently supplied jets.

noncomputable def NavierStokes.ParametricFlatFactor.kernel {E : Type u_1} (c : ℝ) (j : ℕ) (b : E × ℝ → ℝ) (y : E × ℝ) (t : ℝ) : ℝ

Kernel as an element of ℝ.

Equations

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

noncomputable def NavierStokes.ParametricFlatFactor.factor {E : Type u_1} (c : ℝ) (j : ℕ) (b : E × ℝ → ℝ) (y : E × ℝ) : ℝ

Factor, given by ∫ t in Ioi (0 : ℝ), kernel c j b y t.

Equations

• NavierStokes.ParametricFlatFactor.factor c j b y = ∫ (t : ℝ) in Set.Ioi 0, NavierStokes.ParametricFlatFactor.kernel c j b y t

noncomputable def NavierStokes.ParametricFlatFactor.primitive {E : Type u_1} (c : ℝ) (j : ℕ) (b : E × ℝ → ℝ) (y : E × ℝ) : ℝ

Primitive, given by FlatPrimitive.primitive c j (fun u => b (y.1, u)) y.2.

Equations

• NavierStokes.ParametricFlatFactor.primitive c j b y = NavierStokes.FlatPrimitive.primitive c j (fun (u : ℝ) => b (y.1, u)) y.2

theorem NavierStokes.ParametricFlatFactor.factor_eq_scalar {E : Type u_1} (c : ℝ) (j : ℕ) (b : E × ℝ → ℝ) (p : E) (x : ℝ) : factor c j b (p, x) = FlatPrimitiveFactor.factor c j (fun (u : ℝ) => b (p, u)) x

theorem NavierStokes.ParametricFlatFactor.coefficient_slice_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {b : E × ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (p : E) : ContDiff ℝ ↑⊤ fun (u : ℝ) => b (p, u)

theorem NavierStokes.ParametricFlatFactor.factor_slice_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : ℝ} (hc : 0 < c) (j : ℕ) {b : E × ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (p : E) : ContDiff ℝ ↑⊤ fun (x : ℝ) => factor c j b (p, x)

theorem NavierStokes.ParametricFlatFactor.factor_at_zero {E : Type u_1} {c : ℝ} (hc : 0 < c) (j : ℕ) (b : E × ℝ → ℝ) (p : E) : factor c j b (p, 0) = b (p, 0) / (2 * c)

theorem NavierStokes.ParametricFlatFactor.primitive_factorization {E : Type u_1} (c : ℝ) (j : ℕ) (b : E × ℝ → ℝ) (p : E) {x : ℝ} (hx : 0 < x) : FlatPrimitive.primitive c j (fun (u : ℝ) => b (p, u)) x = FlatPrimitive.scale c j x * factor c j b (p, x)

theorem NavierStokes.ParametricFlatFactor.primitive_eq_scale_mul_factor {E : Type u_1} (c : ℝ) (j : ℕ) (b : E × ℝ → ℝ) (y : E × ℝ) : primitive c j b y = FlatPrimitive.scale c j y.2 * factor c j b y

theorem NavierStokes.ParametricFlatFactor.integral_original_factorization {E : Type u_1} (c : ℝ) (j : ℕ) (b : E × ℝ → ℝ) (p : E) {x : ℝ} (hx : 0 < x) : ∫ (u : ℝ) in 0..x, Real.exp (-c / u ^ 2) / u ^ j * b (p, u) = Real.exp (-c / x ^ 2) * x ^ (3 - ↑j) * factor c j b (p, x)

theorem NavierStokes.ParametricFlatFactor.kernel_joint_contDiffAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℝ) (j : ℕ) {b : E × ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (y : E × ℝ) {t : ℝ} (ht : 0 < t) : ContDiffAt ℝ (↑⊤) (fun (q : ℝ × E × ℝ) => kernel c j b q.2 q.1) (t, y)

theorem NavierStokes.ParametricFlatFactor.kernel_contDiff_param {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℝ) (j : ℕ) {b : E × ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) {t : ℝ} (ht : 0 < t) : ContDiff ℝ ↑⊤ fun (y : E × ℝ) => kernel c j b y t

theorem NavierStokes.ParametricFlatFactor.kernel_ae_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℝ) (j : ℕ) {b : E × ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), ContDiff ℝ ↑⊤ fun (y : E × ℝ) => kernel c j b y t

theorem NavierStokes.ParametricFlatFactor.kernel_jet_continuousOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℝ) (j : ℕ) {b : E × ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (n : ℕ) (y : E × ℝ) : ContinuousOn (fun (t : ℝ) => iteratedFDeriv ℝ n (fun (z : E × ℝ) => kernel c j b z t) y) (Set.Ioi 0)

Joint smoothness gives measurability of every actual parameter derivative in the integration variable.

theorem NavierStokes.ParametricFlatFactor.kernel_jet_measurable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℝ) (j : ℕ) {b : E × ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (n : ℕ) (y : E × ℝ) : MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => iteratedFDeriv ℝ n (fun (z : E × ℝ) => kernel c j b z t) y) (MeasureTheory.volume.restrict (Set.Ioi 0))

theorem NavierStokes.ParametricFlatFactor.bounded_coefficient_jets {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {b : E × ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (R : ℝ) (n : ℕ) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ k ≤ n, ∀ (z : E × ℝ), ‖z‖ ≤ R → ‖iteratedFDeriv ℝ k b z‖ ≤ B

Finitely many actual coefficient derivatives have one common bound on each bounded closed parameter-coordinate ball.

theorem NavierStokes.ParametricFlatFactor.kernel_locallyDominated {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {c : ℝ} (hc : 0 < c) (j : ℕ) {b : E × ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) : SmoothParameterIntegral.LocallyDominated (kernel c j b) (MeasureTheory.volume.restrict (Set.Ioi 0))

Uniform bounds for the coefficient jets on compact parameter sets, together with the concrete joint kernel estimate, provide the integrable majorants required for actual Fréchet differentiation under the integral.

theorem NavierStokes.ParametricFlatFactor.factor_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {c : ℝ} (hc : 0 < c) (j : ℕ) {b : E × ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) : ContDiff ℝ (↑⊤) (factor c j b)

The constructed normalized factor is jointly smooth in every auxiliary parameter and the edge coordinate.

theorem NavierStokes.ParametricFlatFactor.factor_iteratedFDeriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {c : ℝ} (hc : 0 < c) (j : ℕ) {b : E × ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (n : ℕ) (y : E × ℝ) : iteratedFDeriv ℝ n (factor c j b) y = ∫ (t : ℝ) in Set.Ioi 0, iteratedFDeriv ℝ n (fun (z : E × ℝ) => kernel c j b z t) y

This formula includes all mixed parameter/edge derivatives as genuine Fréchet derivatives, with the corresponding multilinear maps integrated.

theorem NavierStokes.ParametricFlatFactor.primitive_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {c : ℝ} (hc : 0 < c) (j : ℕ) {b : E × ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) : ContDiff ℝ (↑⊤) (primitive c j b)

theorem NavierStokes.ParametricFlatFactor.exists_joint_smooth_factor {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {c : ℝ} (hc : 0 < c) (j : ℕ) {b : E × ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) : ∃ (F : E × ℝ → ℝ), ContDiff ℝ (↑⊤) F ∧ (∀ (p : E), F (p, 0) = b (p, 0) / (2 * c)) ∧ ∀ (p : E) (x : ℝ), 0 < x → ∫ (u : ℝ) in 0..x, Real.exp (-c / u ^ 2) / u ^ j * b (p, u) = Real.exp (-c / x ^ 2) * x ^ (3 - ↑j) * F (p, x)

Jointly smooth factorization with no assumed factor smoothness or integrable derivative bounds in its hypotheses.

theorem NavierStokes.ParametricFlatFactor.factor_sqrt_contDiffAt_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {c : ℝ} (hc : 0 < c) (j : ℕ) {b : E × ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (p : E) (hbp : 0 < b (p, 0)) : ContDiffAt ℝ (↑⊤) (fun (y : E × ℝ) => √(factor c j b y)) (p, 0)