ContinuousFieldDerivative.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Passing from derivatives along each initial frame to a derivative in the space of continuous fields. The fundamental theorem of calculus avoids any separate uniform remainder assumption.

theorem OAI.PositiveEinsteinFour.Averages.continuousField_hasDerivAt line 25
Source documentation
A continuous family of pointwise derivatives is the derivative in the supremum norm on continuous fields.
```
theorem continuousField_hasDerivAt {F G : ℝ → C(Ω, E)}
    (hG : Continuous G)
    (hpoint : ∀ t x, HasDerivAt (fun s => F s x) (G t x) t) (t : ℝ) :
    HasDerivAt F (G t) t := by
…
```

theorem OAI.PositiveEinsteinFour.Averages.continuousField_hasDerivAt_of_joint line 51

Source documentation

Joint continuity in time and the compact parameter gives exactly the continuity required by continuousField_hasDerivAt.

theorem continuousField_hasDerivAt_of_joint {F G : ℝ → C(Ω, E)}
    (hG : Continuous (fun p : ℝ × Ω => G p.1 p.2))
    (hpoint : ∀ t x, HasDerivAt (fun s => F s x) (G t x) t) (t : ℝ) :
    HasDerivAt F (G t) t :=
…