Time derivatives of integrals with uniform compact spatial support

The public statements use the ordinary volume integral over all of R³. Uniform compact support supplies integrability and a local dominating function.

theorem NavierStokesR3.CompactTimeIntegral.continuous_slice {E : Type u_1} [NormedAddCommGroup E] {F : ℝ × ProblemStatement.Space → E} {s : Set ℝ} (hF : ContinuousOn F (s ×ˢ Set.univ)) {t : ℝ} (ht : t ∈ s) : Continuous fun (x : ProblemStatement.Space) => F (t, x)

Joint continuity on a time set gives continuity of each spatial slice.

theorem NavierStokesR3.CompactTimeIntegral.integrable_slice {E : Type u_1} [NormedAddCommGroup E] {F : ℝ × ProblemStatement.Space → E} {s : Set ℝ} {K : Set ProblemStatement.Space} (hK : IsCompact K) (hF : ContinuousOn F (s ×ˢ Set.univ)) (hsupp : ∀ t ∈ s, ∀ x ∉ K, F (t, x) = 0) {t : ℝ} (ht : t ∈ s) : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => F (t, x)) MeasureTheory.volume

A continuous spatial slice supported in a fixed compact set is integrable.

theorem NavierStokesR3.CompactTimeIntegral.continuousOn_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : ℝ × ProblemStatement.Space → E} {s : Set ℝ} {K : Set ProblemStatement.Space} (hK : IsCompact K) (hF : ContinuousOn F (s ×ˢ Set.univ)) (hsupp : ∀ t ∈ s, ∀ x ∉ K, F (t, x) = 0) : ContinuousOn (fun (t : ℝ) => ∫ (x : ProblemStatement.Space), F (t, x)) s

Ordinary spatial integration preserves continuity on the time set under uniform compact support. In particular the time set may be a closed interval.

theorem NavierStokesR3.CompactTimeIntegral.derivative_eq_zero_outside {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F G : ℝ × ProblemStatement.Space → E} {a b : ℝ} {K : Set ProblemStatement.Space} (hsupp : ∀ t ∈ Set.Ioo a b, ∀ x ∉ K, F (t, x) = 0) (hderiv : ∀ t ∈ Set.Ioo a b, ∀ (x : ProblemStatement.Space), HasDerivAt (fun (r : ℝ) => F (r, x)) (G (t, x)) t) {t : ℝ} (ht : t ∈ Set.Ioo a b) {x : ProblemStatement.Space} (hx : x ∉ K) : G (t, x) = 0

A time derivative vanishes outside the uniform spatial support at every interior time.

theorem NavierStokesR3.CompactTimeIntegral.hasDerivAt_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F G : ℝ × ProblemStatement.Space → E} {a b t : ℝ} {K : Set ProblemStatement.Space} (hK : IsCompact K) (hF : ContinuousOn F (Set.Ioo a b ×ˢ Set.univ)) (hG : ContinuousOn G (Set.Ioo a b ×ˢ Set.univ)) (hsupp : ∀ r ∈ Set.Ioo a b, ∀ x ∉ K, F (r, x) = 0) (hderiv : ∀ r ∈ Set.Ioo a b, ∀ (x : ProblemStatement.Space), HasDerivAt (fun (q : ℝ) => F (q, x)) (G (r, x)) r) (ht : t ∈ Set.Ioo a b) : HasDerivAt (fun (r : ℝ) => ∫ (x : ProblemStatement.Space), F (r, x)) (∫ (x : ProblemStatement.Space), G (t, x)) t

Differentiation under the ordinary spatial integral. Joint continuity of the field and its time derivative is needed only at interior times.

theorem NavierStokesR3.CompactTimeIntegral.hasDerivAt_time_of_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : ℝ × ProblemStatement.Space → E} {a b t : ℝ} (hF : ContDiffOn ℝ 1 F (Set.Icc a b ×ˢ Set.univ)) (ht : t ∈ Set.Ioo a b) (x : ProblemStatement.Space) : HasDerivAt (fun (r : ℝ) => F (r, x)) ((fderiv ℝ F (t, x)) (1, 0)) t

The time derivative of a jointly C¹ field at an interior time is the full derivative evaluated on the time direction.

theorem NavierStokesR3.CompactTimeIntegral.continuousOn_timeFDeriv_of_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : ℝ × ProblemStatement.Space → E} {a b : ℝ} (hF : ContDiffOn ℝ 1 F (Set.Icc a b ×ˢ Set.univ)) : ContinuousOn (fun (p : ℝ × ProblemStatement.Space) => (fderiv ℝ F p) (1, 0)) (Set.Ioo a b ×ˢ Set.univ)

The time component of the full derivative is jointly continuous in the interior of the time slab.

theorem NavierStokesR3.CompactTimeIntegral.continuousOn_timeDeriv_of_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : ℝ × ProblemStatement.Space → E} {a b : ℝ} (hF : ContDiffOn ℝ 1 F (Set.Icc a b ×ˢ Set.univ)) : ContinuousOn (fun (p : ℝ × ProblemStatement.Space) => deriv (fun (r : ℝ) => F (r, p.2)) p.1) (Set.Ioo a b ×ˢ Set.univ)

The ordinary one-dimensional time derivative of a jointly C¹ field is jointly continuous at interior times.

theorem NavierStokesR3.CompactTimeIntegral.continuousOn_integral_of_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : ℝ × ProblemStatement.Space → E} {a b : ℝ} {K : Set ProblemStatement.Space} (hK : IsCompact K) (hF : ContDiffOn ℝ 1 F (Set.Icc a b ×ˢ Set.univ)) (hsupp : ∀ t ∈ Set.Icc a b, ∀ x ∉ K, F (t, x) = 0) : ContinuousOn (fun (t : ℝ) => ∫ (x : ProblemStatement.Space), F (t, x)) (Set.Icc a b)

A jointly C¹ field with uniform compact spatial support has a continuous ordinary spatial integral throughout the closed time slab.

theorem NavierStokesR3.CompactTimeIntegral.hasDerivAt_integral_of_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : ℝ × ProblemStatement.Space → E} {a b t : ℝ} {K : Set ProblemStatement.Space} (hK : IsCompact K) (hF : ContDiffOn ℝ 1 F (Set.Icc a b ×ˢ Set.univ)) (hsupp : ∀ r ∈ Set.Icc a b, ∀ x ∉ K, F (r, x) = 0) (ht : t ∈ Set.Ioo a b) : HasDerivAt (fun (r : ℝ) => ∫ (x : ProblemStatement.Space), F (r, x)) (∫ (x : ProblemStatement.Space), deriv (fun (r : ℝ) => F (r, x)) t) t

At interior times, the derivative of the ordinary spatial integral is the integral of the ordinary time derivative.

theorem NavierStokesR3.CompactTimeIntegral.hasDerivAt_integral_of_contDiffOn_of_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : ℝ × ProblemStatement.Space → E} {G : ProblemStatement.Space → E} {a b t : ℝ} {K : Set ProblemStatement.Space} (hK : IsCompact K) (hF : ContDiffOn ℝ 1 F (Set.Icc a b ×ˢ Set.univ)) (hsupp : ∀ r ∈ Set.Icc a b, ∀ x ∉ K, F (r, x) = 0) (ht : t ∈ Set.Ioo a b) (hderiv : ∀ (x : ProblemStatement.Space), HasDerivAt (fun (r : ℝ) => F (r, x)) (G x) t) : HasDerivAt (fun (r : ℝ) => ∫ (x : ProblemStatement.Space), F (r, x)) (∫ (x : ProblemStatement.Space), G x) t

A convenient form of differentiation under the spatial integral in which the derivative is supplied pointwise only at the time being considered.