Smooth parameter integrals with local integrable majorants

The Taylor coefficients below are integrals of the actual iteratedFDeriv of the integrand. Their successive derivative relation is proved using dominated differentiation and the currying identity for iteratedFDeriv; it is not an assumption on a separately supplied family of jets.

noncomputable def NavierStokes.SmoothParameterIntegral.jet {α : Type u_1} {H : Type u_2} {E : Type u_3} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup E] [NormedSpace ℝ E] (F : H → α → E) (k : ℕ) (x : H) (t : α) : H [×k]→L[ℝ] E

The genuine derivative in the parameter, with the integration variable last.

Equations

• NavierStokes.SmoothParameterIntegral.jet F k x t = iteratedFDeriv ℝ k (fun (y : H) => F y t) x

def NavierStokes.SmoothParameterIntegral.LocallyDominated {α : Type u_1} {H : Type u_2} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup E] [NormedSpace ℝ E] (F : H → α → E) (μ : MeasureTheory.Measure α) : Prop

Each order has an integrable majorant on a neighborhood of each parameter. The neighborhood is uniform in the integration variable; it may depend on the order and the center.

Equations

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

theorem NavierStokes.SmoothParameterIntegral.integrable_jet {α : Type u_1} {H : Type u_2} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup E] [NormedSpace ℝ E] {F : H → α → E} {μ : MeasureTheory.Measure α} (h_meas : ∀ (k : ℕ) (x : H), MeasureTheory.AEStronglyMeasurable (jet F k x) μ) (h_dom : LocallyDominated F μ) (k : ℕ) (x : H) : MeasureTheory.Integrable (jet F k x) μ

theorem NavierStokes.SmoothParameterIntegral.hasFDerivAt_integral_jet {α : Type u_1} {H : Type u_2} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup E] [NormedSpace ℝ E] {F : H → α → E} {μ : MeasureTheory.Measure α} (h_smooth : ∀ᵐ (t : α) ∂μ, ContDiff ℝ ↑⊤ fun (x : H) => F x t) (h_meas : ∀ (k : ℕ) (x : H), MeasureTheory.AEStronglyMeasurable (jet F k x) μ) (h_dom : LocallyDominated F μ) (k : ℕ) (x : H) : HasFDerivAt (fun (y : H) => ∫ (t : α), jet F k y t ∂μ) (∫ (t : α), jet F (k + 1) x t ∂μ).curryLeft x

Differentiation of every integrated genuine jet, with the correct curry map.

theorem NavierStokes.SmoothParameterIntegral.hasFTaylorSeriesUpTo_integral {α : Type u_1} {H : Type u_2} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup E] [NormedSpace ℝ E] {F : H → α → E} {μ : MeasureTheory.Measure α} (h_smooth : ∀ᵐ (t : α) ∂μ, ContDiff ℝ ↑⊤ fun (x : H) => F x t) (h_meas : ∀ (k : ℕ) (x : H), MeasureTheory.AEStronglyMeasurable (jet F k x) μ) (h_dom : LocallyDominated F μ) : HasFTaylorSeriesUpTo (↑⊤) (fun (x : H) => ∫ (t : α), F x t ∂μ) fun (x : H) (k : ℕ) => ∫ (t : α), jet F k x t ∂μ

The Taylor series consists of the integrated genuine derivatives.

theorem NavierStokes.SmoothParameterIntegral.contDiff_integral {α : Type u_1} {H : Type u_2} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup E] [NormedSpace ℝ E] {F : H → α → E} {μ : MeasureTheory.Measure α} (h_smooth : ∀ᵐ (t : α) ∂μ, ContDiff ℝ ↑⊤ fun (x : H) => F x t) (h_meas : ∀ (k : ℕ) (x : H), MeasureTheory.AEStronglyMeasurable (jet F k x) μ) (h_dom : LocallyDominated F μ) : ContDiff ℝ ↑⊤ fun (x : H) => ∫ (t : α), F x t ∂μ

theorem NavierStokes.SmoothParameterIntegral.iteratedFDeriv_integral {α : Type u_1} {H : Type u_2} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup E] [NormedSpace ℝ E] {F : H → α → E} {μ : MeasureTheory.Measure α} (h_smooth : ∀ᵐ (t : α) ∂μ, ContDiff ℝ ↑⊤ fun (x : H) => F x t) (h_meas : ∀ (k : ℕ) (x : H), MeasureTheory.AEStronglyMeasurable (jet F k x) μ) (h_dom : LocallyDominated F μ) (k : ℕ) (x : H) : iteratedFDeriv ℝ k (fun (y : H) => ∫ (t : α), F y t ∂μ) x = ∫ (t : α), iteratedFDeriv ℝ k (fun (y : H) => F y t) x ∂μ

def NavierStokes.SmoothParameterIntegral.LocallyDominatedOn {α : Type u_1} {H : Type u_2} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup E] [NormedSpace ℝ E] (F : H → α → E) (μ : MeasureTheory.Measure α) (s : Set H) : Prop

Local domination on an open parameter domain. The dominating ball is explicitly contained in that domain; no behavior outside it is prescribed.

Equations

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

theorem NavierStokes.SmoothParameterIntegral.integrable_jetOn {α : Type u_1} {H : Type u_2} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup E] [NormedSpace ℝ E] {F : H → α → E} {μ : MeasureTheory.Measure α} {s : Set H} (h_meas : ∀ (k : ℕ), ∀ x ∈ s, MeasureTheory.AEStronglyMeasurable (jet F k x) μ) (h_dom : LocallyDominatedOn F μ s) (k : ℕ) {x : H} (hx : x ∈ s) : MeasureTheory.Integrable (jet F k x) μ

theorem NavierStokes.SmoothParameterIntegral.hasFDerivAt_integral_jetOn {α : Type u_1} {H : Type u_2} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup E] [NormedSpace ℝ E] {F : H → α → E} {μ : MeasureTheory.Measure α} {s : Set H} (hs : IsOpen s) (h_smooth : ∀ᵐ (t : α) ∂μ, ContDiffOn ℝ (↑⊤) (fun (x : H) => F x t) s) (h_meas : ∀ (k : ℕ), ∀ x ∈ s, MeasureTheory.AEStronglyMeasurable (jet F k x) μ) (h_dom : LocallyDominatedOn F μ s) (k : ℕ) {x : H} (hx : x ∈ s) : HasFDerivAt (fun (y : H) => ∫ (t : α), jet F k y t ∂μ) (∫ (t : α), jet F (k + 1) x t ∂μ).curryLeft x

theorem NavierStokes.SmoothParameterIntegral.hasFTaylorSeriesUpToOn_integral {α : Type u_1} {H : Type u_2} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup E] [NormedSpace ℝ E] {F : H → α → E} {μ : MeasureTheory.Measure α} {s : Set H} (hs : IsOpen s) (h_smooth : ∀ᵐ (t : α) ∂μ, ContDiffOn ℝ (↑⊤) (fun (x : H) => F x t) s) (h_meas : ∀ (k : ℕ), ∀ x ∈ s, MeasureTheory.AEStronglyMeasurable (jet F k x) μ) (h_dom : LocallyDominatedOn F μ s) : HasFTaylorSeriesUpToOn (↑⊤) (fun (x : H) => ∫ (t : α), F x t ∂μ) (fun (x : H) (k : ℕ) => ∫ (t : α), jet F k x t ∂μ) s

theorem NavierStokes.SmoothParameterIntegral.contDiffOn_integral {α : Type u_1} {H : Type u_2} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup E] [NormedSpace ℝ E] {F : H → α → E} {μ : MeasureTheory.Measure α} {s : Set H} (hs : IsOpen s) (h_smooth : ∀ᵐ (t : α) ∂μ, ContDiffOn ℝ (↑⊤) (fun (x : H) => F x t) s) (h_meas : ∀ (k : ℕ), ∀ x ∈ s, MeasureTheory.AEStronglyMeasurable (jet F k x) μ) (h_dom : LocallyDominatedOn F μ s) : ContDiffOn ℝ (↑⊤) (fun (x : H) => ∫ (t : α), F x t ∂μ) s

theorem NavierStokes.SmoothParameterIntegral.iteratedFDeriv_integralOn {α : Type u_1} {H : Type u_2} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup E] [NormedSpace ℝ E] {F : H → α → E} {μ : MeasureTheory.Measure α} {s : Set H} (hs : IsOpen s) (h_smooth : ∀ᵐ (t : α) ∂μ, ContDiffOn ℝ (↑⊤) (fun (x : H) => F x t) s) (h_meas : ∀ (k : ℕ), ∀ x ∈ s, MeasureTheory.AEStronglyMeasurable (jet F k x) μ) (h_dom : LocallyDominatedOn F μ s) (k : ℕ) {x : H} (hx : x ∈ s) : iteratedFDeriv ℝ k (fun (y : H) => ∫ (t : α), F y t ∂μ) x = ∫ (t : α), iteratedFDeriv ℝ k (fun (y : H) => F y t) x ∂μ

theorem NavierStokes.SmoothParameterIntegral.contDiffOn_integral_Ioc_of_continuous_jet {H : Type u_2} {E : Type u_3} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup E] [NormedSpace ℝ E] [ProperSpace H] {F : H → ℝ → E} {s : Set H} {a b : ℝ} (hs : IsOpen s) (h_smooth : ∀ t ∈ Set.Icc a b, ContDiffOn ℝ (↑⊤) (fun (x : H) => F x t) s) (h_jet : ∀ (k : ℕ), ContinuousOn (fun (z : H × ℝ) => jet F k z.1 z.2) (s ×ˢ Set.Icc a b)) : ContDiffOn ℝ (↑⊤) (fun (x : H) => ∫ (t : ℝ) in Set.Ioc a b, F x t) s

On a compact integration interval, joint continuity of the actual parameter jets supplies all local majorants. Properness is automatic for finite-dimensional real normed parameter spaces.

theorem NavierStokes.SmoothParameterIntegral.contDiffOn_intervalIntegral_of_continuous_jet {H : Type u_2} {E : Type u_3} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup E] [NormedSpace ℝ E] [ProperSpace H] {F : H → ℝ → E} {s : Set H} {a b : ℝ} (hs : IsOpen s) (hab : a ≤ b) (h_smooth : ∀ t ∈ Set.Icc a b, ContDiffOn ℝ (↑⊤) (fun (x : H) => F x t) s) (h_jet : ∀ (k : ℕ), ContinuousOn (fun (z : H × ℝ) => jet F k z.1 z.2) (s ×ˢ Set.Icc a b)) : ContDiffOn ℝ (↑⊤) (fun (x : H) => ∫ (t : ℝ) in a..b, F x t) s

def NavierStokes.SmoothParameterIntegral.LocallyDominatedDeriv {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] (F : ℝ → α → E) (μ : MeasureTheory.Measure α) : Prop

One-dimensional form of the same local domination condition, using actual scalar iterated derivatives rather than multilinear maps.

Equations

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

theorem NavierStokes.SmoothParameterIntegral.LocallyDominatedDeriv.toLocallyDominated {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure α} {F : ℝ → α → E} (h : LocallyDominatedDeriv F μ) : LocallyDominated F μ

theorem NavierStokes.SmoothParameterIntegral.aestronglyMeasurable_jet_of_iteratedDeriv {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure α} {F : ℝ → α → E} (h : ∀ (k : ℕ) (x : ℝ), MeasureTheory.AEStronglyMeasurable (fun (t : α) => iteratedDeriv k (fun (y : ℝ) => F y t) x) μ) (k : ℕ) (x : ℝ) : MeasureTheory.AEStronglyMeasurable (jet F k x) μ

theorem NavierStokes.SmoothParameterIntegral.contDiff_integral_of_iteratedDeriv {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure α} {F : ℝ → α → E} (h_smooth : ∀ᵐ (t : α) ∂μ, ContDiff ℝ ↑⊤ fun (x : ℝ) => F x t) (h_meas : ∀ (k : ℕ) (x : ℝ), MeasureTheory.AEStronglyMeasurable (fun (t : α) => iteratedDeriv k (fun (y : ℝ) => F y t) x) μ) (h_dom : LocallyDominatedDeriv F μ) : ContDiff ℝ ↑⊤ fun (x : ℝ) => ∫ (t : α), F x t ∂μ

The scalar-parameter interface can be applied directly to a restricted Lebesgue measure, including volume.restrict (Ioi 0).

theorem NavierStokes.SmoothParameterIntegral.iteratedDeriv_integral {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure α} {F : ℝ → α → E} (h_smooth : ∀ᵐ (t : α) ∂μ, ContDiff ℝ ↑⊤ fun (x : ℝ) => F x t) (h_meas : ∀ (k : ℕ) (x : ℝ), MeasureTheory.AEStronglyMeasurable (fun (t : α) => iteratedDeriv k (fun (y : ℝ) => F y t) x) μ) (h_dom : LocallyDominatedDeriv F μ) (k : ℕ) (x : ℝ) : iteratedDeriv k (fun (y : ℝ) => ∫ (t : α), F y t ∂μ) x = ∫ (t : α), iteratedDeriv k (fun (y : ℝ) => F y t) x ∂μ