CompactFluxDifferentiation.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.CompactFluxDifferentiation.continuous_slice line 17
lemma OAI.CompactFluxDifferentiation.integrable_slice line 21

theorem OAI.CompactFluxDifferentiation.continuousOn_integral line 29

Source documentation

Continuity includes both endpoints of the compact parameter interval.

theorem continuousOn_integral
    (hF : ContinuousOn (fun p : ℝ × X => F p.1 p.2) (Icc a b ×ˢ univ)) :
    ContinuousOn (fun s => ∫ x, F s x ∂μ) (Icc a b) := by
…

theorem OAI.CompactFluxDifferentiation.continuous_integral line 45
Source documentation
The local compact-interval argument also gives continuity on the full line.
```
theorem continuous_integral
    (hF : Continuous (fun p : ℝ × X => F p.1 p.2)) :
    Continuous (fun s => ∫ x, F s x ∂μ) := by
…
```

theorem OAI.CompactFluxDifferentiation.hasDerivAt_integral line 55

Source documentation

Joint continuity on a compact parameter interval and compact finite-measure fiber supplies every domination and measurability obligation.

theorem hasDerivAt_integral
    (hF : ContinuousOn (fun p : ℝ × X => F p.1 p.2) (Icc a b ×ˢ univ))
    (hG : ContinuousOn (fun p : ℝ × X => G p.1 p.2) (Icc a b ×ˢ univ))
    (hd : ∀ s ∈ Ioo a b, ∀ x, HasDerivAt (fun r => F r x) (G s x) s)
    (ht : t ∈ Ioo a b) :
    HasDerivAt (fun s => ∫ x, F s x ∂μ) (∫ x, G t x ∂μ) t := by
…