BoundedSpatialJetIntegral.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Integrating time-dependent sources in the finite spatial jet Banach space.

theorem OAI.ForcedComputation.BoundedSpatialJets.function_intervalIntegral line 18
Source documentation
Time integration commutes with pointwise evaluation of the represented function.
```
theorem function_intervalIntegral (k : ℕ) (J : ℝ → Space E F k) (a b : ℝ)
    (hJ : IntervalIntegrable J volume a b) (x : E) :
    function E F k (∫ t in a..b, J t) x =
      ∫ t in a..b, function E F k (J t) x := by
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space, OAI.ForcedComputation.BoundedSpatialJets.function

theorem OAI.ForcedComputation.BoundedSpatialJets.jet_intervalIntegral line 27

Source documentation

Every recorded spatial jet commutes with time integration.

theorem jet_intervalIntegral (k : ℕ) (J : ℝ → Space E F k) (a b : ℝ)
    (hJ : IntervalIntegrable J volume a b) (i : Fin (k + 1)) (x : E) :
    (∫ t in a..b, J t).val i x = ∫ t in a..b, (J t).val i x := by
…

Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space

theorem OAI.ForcedComputation.BoundedSpatialJets.iteratedFDeriv_intervalIntegral line 35

Source documentation

Time integration preserves all spatial derivatives through the selected finite order.

theorem iteratedFDeriv_intervalIntegral (k : ℕ) (J : ℝ → Space E F k) (a b : ℝ)
    (hJ : IntervalIntegrable J volume a b) (n : ℕ) (hn : n ≤ k) (x : E) :
    iteratedFDeriv ℝ n (function E F k (∫ t in a..b, J t)) x =
      ∫ t in a..b, iteratedFDeriv ℝ n (function E F k (J t)) x := by
…

Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space, OAI.ForcedComputation.BoundedSpatialJets.function

theorem OAI.ForcedComputation.BoundedSpatialJets.norm_intervalIntegral_le line 44
Source documentation
A uniform source bound gives the exact interval-length bound in the jet norm.
```
theorem norm_intervalIntegral_le (k : ℕ) (J : ℝ → Space E F k) (a b C : ℝ)
    (hJ : ∀ t ∈ Set.uIoc a b, ‖J t‖ ≤ C) :
    ‖∫ t in a..b, J t‖ ≤ C * |b - a| :=
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space

theorem OAI.ForcedComputation.BoundedSpatialJets.intervalIntegrable_bilinear line 54

Source documentation

A time-dependent coefficient and unknown yield an integrable jet-valued source.

theorem intervalIntegrable_bilinear (k : ℕ) (B : F →L[ℝ] G →L[ℝ] H)
    (J : ℝ → Space E F k) (K : ℝ → Space E G k) (a b : ℝ)
    (hJ : ContinuousOn J (Set.uIcc a b)) (hK : ContinuousOn K (Set.uIcc a b)) :
    IntervalIntegrable (fun t => bilinear E F G H k B (J t) (K t)) volume a b :=
…

Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space, OAI.ForcedComputation.BoundedSpatialJets.bilinear

theorem OAI.ForcedComputation.BoundedSpatialJets.norm_intervalIntegral_bilinear_le line 62

Source documentation

Explicit finite-time source bound, with the finite-order Leibniz constant.

theorem norm_intervalIntegral_bilinear_le (k : ℕ) (B : F →L[ℝ] G →L[ℝ] H)
    (J : ℝ → Space E F k) (K : ℝ → Space E G k) (a b A C : ℝ)
    (hC : 0 ≤ C) (hJ : ∀ t ∈ Set.uIoc a b, ‖J t‖ ≤ A)
    (hK : ∀ t ∈ Set.uIoc a b, ‖K t‖ ≤ C) :
    ‖∫ t in a..b, bilinear E F G H k B (J t) (K t)‖ ≤
      (‖B‖ * (2 : ℝ) ^ k * A * C) * |b - a| := by
…

Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space, OAI.ForcedComputation.BoundedSpatialJets.bilinear