Theorem: has_deriv_at_integral_of_continuous_of_lip (RMT4/to_mathlib.lean)

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a✝ b✝ t : ℝ
n : ℕ
φ : ℂ → ℝ → ℂ
ψ : ℝ → ℂ
z₀ : ℂ
a b C δ : ℝ
hab : a ≤ b
δ_pos : 0 < δ
φ_cts : ∀ᶠ (z : ℂ) in 𝓝 z₀, ContinuousOn (φ z) (Icc a b)
φ_der : ∀ t ∈ Ioc a b, HasDerivAt (fun x => φ x t) (ψ t) z₀
φ_lip : ∀ t ∈ Ioc a b, LipschitzOnWith (nnabs C) (fun x => φ x t) (ball z₀ δ)
ψ_cts : ContinuousOn ψ (Ioc a b)
⊢ HasDerivAt (fun z => ∫ (t : ℝ) in a..b, φ z t) (∫ (t : ℝ) in a..b, ψ t) z₀
Tactic:
simp only [intervalIntegral, not_lt, hab, Ioc_eq_empty, Measure.restrict_empty,
  integral_zero_measure, sub_zero]
State after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a✝ b✝ t : ℝ
n : ℕ
φ : ℂ → ℝ → ℂ
ψ : ℝ → ℂ
z₀ : ℂ
a b C δ : ℝ
hab : a ≤ b
δ_pos : 0 < δ
φ_cts : ∀ᶠ (z : ℂ) in 𝓝 z₀, ContinuousOn (φ z) (Icc a b)
φ_der : ∀ t ∈ Ioc a b, HasDerivAt (fun x => φ x t) (ψ t) z₀
φ_lip : ∀ t ∈ Ioc a b, LipschitzOnWith (nnabs C) (fun x => φ x t) (ball z₀ δ)
ψ_cts : ContinuousOn ψ (Ioc a b)
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioc a b, φ z x ∂volume) (∫ (x : ℝ) in Ioc a b, ψ x ∂volume) z₀

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a✝ b✝ t : ℝ
n : ℕ
φ : ℂ → ℝ → ℂ
ψ : ℝ → ℂ
z₀ : ℂ
a b C δ : ℝ
hab : a ≤ b
δ_pos : 0 < δ
φ_cts : ∀ᶠ (z : ℂ) in 𝓝 z₀, ContinuousOn (φ z) (Icc a b)
φ_der : ∀ t ∈ Ioc a b, HasDerivAt (fun x => φ x t) (ψ t) z₀
φ_lip : ∀ t ∈ Ioc a b, LipschitzOnWith (nnabs C) (fun x => φ x t) (ball z₀ δ)
ψ_cts : ContinuousOn ψ (Ioc a b)
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioc a b, φ z x ∂volume) (∫ (x : ℝ) in Ioc a b, ψ x ∂volume) z₀
Tactic:
let μ : Measure ℝ := volume.restrict (Ioc a b)
State after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a✝ b✝ t : ℝ
n : ℕ
φ : ℂ → ℝ → ℂ
ψ : ℝ → ℂ
z₀ : ℂ
a b C δ : ℝ
hab : a ≤ b
δ_pos : 0 < δ
φ_cts : ∀ᶠ (z : ℂ) in 𝓝 z₀, ContinuousOn (φ z) (Icc a b)
φ_der : ∀ t ∈ Ioc a b, HasDerivAt (fun x => φ x t) (ψ t) z₀
φ_lip : ∀ t ∈ Ioc a b, LipschitzOnWith (nnabs C) (fun x => φ x t) (ball z₀ δ)
ψ_cts : ContinuousOn ψ (Ioc a b)
μ : Measure ℝ := Measure.restrict volume (Ioc a b)
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioc a b, φ z x ∂volume) (∫ (x : ℝ) in Ioc a b, ψ x ∂volume) z₀

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a✝ b✝ t : ℝ
n : ℕ
φ : ℂ → ℝ → ℂ
ψ : ℝ → ℂ
z₀ : ℂ
a b C δ : ℝ
hab : a ≤ b
δ_pos : 0 < δ
φ_cts : ∀ᶠ (z : ℂ) in 𝓝 z₀, ContinuousOn (φ z) (Icc a b)
φ_der : ∀ t ∈ Ioc a b, HasDerivAt (fun x => φ x t) (ψ t) z₀
φ_lip : ∀ t ∈ Ioc a b, LipschitzOnWith (nnabs C) (fun x => φ x t) (ball z₀ δ)
ψ_cts : ContinuousOn ψ (Ioc a b)
μ : Measure ℝ := Measure.restrict volume (Ioc a b)
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioc a b, φ z x ∂volume) (∫ (x : ℝ) in Ioc a b, ψ x ∂volume) z₀
Tactic:
have h1 : ∀ᶠ z in 𝓝 z₀, AEStronglyMeasurable (φ z) μ :=
  φ_cts.mono (λ z h => (h.mono Ioc_subset_Icc_self).aestronglyMeasurable measurableSet_Ioc)
State after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a✝ b✝ t : ℝ
n : ℕ
φ : ℂ → ℝ → ℂ
ψ : ℝ → ℂ
z₀ : ℂ
a b C δ : ℝ
hab : a ≤ b
δ_pos : 0 < δ
φ_cts : ∀ᶠ (z : ℂ) in 𝓝 z₀, ContinuousOn (φ z) (Icc a b)
φ_der : ∀ t ∈ Ioc a b, HasDerivAt (fun x => φ x t) (ψ t) z₀
φ_lip : ∀ t ∈ Ioc a b, LipschitzOnWith (nnabs C) (fun x => φ x t) (ball z₀ δ)
ψ_cts : ContinuousOn ψ (Ioc a b)
μ : Measure ℝ := Measure.restrict volume (Ioc a b)
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AEStronglyMeasurable (φ z) μ
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioc a b, φ z x ∂volume) (∫ (x : ℝ) in Ioc a b, ψ x ∂volume) z₀

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a✝ b✝ t : ℝ
n : ℕ
φ : ℂ → ℝ → ℂ
ψ : ℝ → ℂ
z₀ : ℂ
a b C δ : ℝ
hab : a ≤ b
δ_pos : 0 < δ
φ_cts : ∀ᶠ (z : ℂ) in 𝓝 z₀, ContinuousOn (φ z) (Icc a b)
φ_der : ∀ t ∈ Ioc a b, HasDerivAt (fun x => φ x t) (ψ t) z₀
φ_lip : ∀ t ∈ Ioc a b, LipschitzOnWith (nnabs C) (fun x => φ x t) (ball z₀ δ)
ψ_cts : ContinuousOn ψ (Ioc a b)
μ : Measure ℝ := Measure.restrict volume (Ioc a b)
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AEStronglyMeasurable (φ z) μ
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioc a b, φ z x ∂volume) (∫ (x : ℝ) in Ioc a b, ψ x ∂volume) z₀
Tactic:
have h2 : Integrable (φ z₀) μ :=
  φ_cts.self_of_nhds.integrableOn_Icc.mono_set Ioc_subset_Icc_self
State after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a✝ b✝ t : ℝ
n : ℕ
φ : ℂ → ℝ → ℂ
ψ : ℝ → ℂ
z₀ : ℂ
a b C δ : ℝ
hab : a ≤ b
δ_pos : 0 < δ
φ_cts : ∀ᶠ (z : ℂ) in 𝓝 z₀, ContinuousOn (φ z) (Icc a b)
φ_der : ∀ t ∈ Ioc a b, HasDerivAt (fun x => φ x t) (ψ t) z₀
φ_lip : ∀ t ∈ Ioc a b, LipschitzOnWith (nnabs C) (fun x => φ x t) (ball z₀ δ)
ψ_cts : ContinuousOn ψ (Ioc a b)
μ : Measure ℝ := Measure.restrict volume (Ioc a b)
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AEStronglyMeasurable (φ z) μ
h2 : Integrable (φ z₀) μ
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioc a b, φ z x ∂volume) (∫ (x : ℝ) in Ioc a b, ψ x ∂volume) z₀

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a✝ b✝ t : ℝ
n : ℕ
φ : ℂ → ℝ → ℂ
ψ : ℝ → ℂ
z₀ : ℂ
a b C δ : ℝ
hab : a ≤ b
δ_pos : 0 < δ
φ_cts : ∀ᶠ (z : ℂ) in 𝓝 z₀, ContinuousOn (φ z) (Icc a b)
φ_der : ∀ t ∈ Ioc a b, HasDerivAt (fun x => φ x t) (ψ t) z₀
φ_lip : ∀ t ∈ Ioc a b, LipschitzOnWith (nnabs C) (fun x => φ x t) (ball z₀ δ)
ψ_cts : ContinuousOn ψ (Ioc a b)
μ : Measure ℝ := Measure.restrict volume (Ioc a b)
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AEStronglyMeasurable (φ z) μ
h2 : Integrable (φ z₀) μ
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioc a b, φ z x ∂volume) (∫ (x : ℝ) in Ioc a b, ψ x ∂volume) z₀
Tactic:
have h3 : AEStronglyMeasurable ψ μ := ψ_cts.aestronglyMeasurable measurableSet_Ioc
State after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a✝ b✝ t : ℝ
n : ℕ
φ : ℂ → ℝ → ℂ
ψ : ℝ → ℂ
z₀ : ℂ
a b C δ : ℝ
hab : a ≤ b
δ_pos : 0 < δ
φ_cts : ∀ᶠ (z : ℂ) in 𝓝 z₀, ContinuousOn (φ z) (Icc a b)
φ_der : ∀ t ∈ Ioc a b, HasDerivAt (fun x => φ x t) (ψ t) z₀
φ_lip : ∀ t ∈ Ioc a b, LipschitzOnWith (nnabs C) (fun x => φ x t) (ball z₀ δ)
ψ_cts : ContinuousOn ψ (Ioc a b)
μ : Measure ℝ := Measure.restrict volume (Ioc a b)
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AEStronglyMeasurable (φ z) μ
h2 : Integrable (φ z₀) μ
h3 : AEStronglyMeasurable ψ μ
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioc a b, φ z x ∂volume) (∫ (x : ℝ) in Ioc a b, ψ x ∂volume) z₀

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a✝ b✝ t : ℝ
n : ℕ
φ : ℂ → ℝ → ℂ
ψ : ℝ → ℂ
z₀ : ℂ
a b C δ : ℝ
hab : a ≤ b
δ_pos : 0 < δ
φ_cts : ∀ᶠ (z : ℂ) in 𝓝 z₀, ContinuousOn (φ z) (Icc a b)
φ_der : ∀ t ∈ Ioc a b, HasDerivAt (fun x => φ x t) (ψ t) z₀
φ_lip : ∀ t ∈ Ioc a b, LipschitzOnWith (nnabs C) (fun x => φ x t) (ball z₀ δ)
ψ_cts : ContinuousOn ψ (Ioc a b)
μ : Measure ℝ := Measure.restrict volume (Ioc a b)
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AEStronglyMeasurable (φ z) μ
h2 : Integrable (φ z₀) μ
h3 : AEStronglyMeasurable ψ μ
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioc a b, φ z x ∂volume) (∫ (x : ℝ) in Ioc a b, ψ x ∂volume) z₀
Tactic:
have h4 : ∀ᵐ t ∂μ, LipschitzOnWith (Real.nnabs C) (λ z => φ z t) (ball z₀ δ) :=
  (ae_restrict_iff' measurableSet_Ioc).mpr (eventually_of_forall φ_lip)
State after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a✝ b✝ t : ℝ
n : ℕ
φ : ℂ → ℝ → ℂ
ψ : ℝ → ℂ
z₀ : ℂ
a b C δ : ℝ
hab : a ≤ b
δ_pos : 0 < δ
φ_cts : ∀ᶠ (z : ℂ) in 𝓝 z₀, ContinuousOn (φ z) (Icc a b)
φ_der : ∀ t ∈ Ioc a b, HasDerivAt (fun x => φ x t) (ψ t) z₀
φ_lip : ∀ t ∈ Ioc a b, LipschitzOnWith (nnabs C) (fun x => φ x t) (ball z₀ δ)
ψ_cts : ContinuousOn ψ (Ioc a b)
μ : Measure ℝ := Measure.restrict volume (Ioc a b)
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AEStronglyMeasurable (φ z) μ
h2 : Integrable (φ z₀) μ
h3 : AEStronglyMeasurable ψ μ
h4 : ∀ᵐ (t : ℝ) ∂μ, LipschitzOnWith (nnabs C) (fun z => φ z t) (ball z₀ δ)
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioc a b, φ z x ∂volume) (∫ (x : ℝ) in Ioc a b, ψ x ∂volume) z₀

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a✝ b✝ t : ℝ
n : ℕ
φ : ℂ → ℝ → ℂ
ψ : ℝ → ℂ
z₀ : ℂ
a b C δ : ℝ
hab : a ≤ b
δ_pos : 0 < δ
φ_cts : ∀ᶠ (z : ℂ) in 𝓝 z₀, ContinuousOn (φ z) (Icc a b)
φ_der : ∀ t ∈ Ioc a b, HasDerivAt (fun x => φ x t) (ψ t) z₀
φ_lip : ∀ t ∈ Ioc a b, LipschitzOnWith (nnabs C) (fun x => φ x t) (ball z₀ δ)
ψ_cts : ContinuousOn ψ (Ioc a b)
μ : Measure ℝ := Measure.restrict volume (Ioc a b)
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AEStronglyMeasurable (φ z) μ
h2 : Integrable (φ z₀) μ
h3 : AEStronglyMeasurable ψ μ
h4 : ∀ᵐ (t : ℝ) ∂μ, LipschitzOnWith (nnabs C) (fun z => φ z t) (ball z₀ δ)
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioc a b, φ z x ∂volume) (∫ (x : ℝ) in Ioc a b, ψ x ∂volume) z₀
Tactic:
have h5 : Integrable (λ _ => C) μ := integrable_const _
State after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a✝ b✝ t : ℝ
n : ℕ
φ : ℂ → ℝ → ℂ
ψ : ℝ → ℂ
z₀ : ℂ
a b C δ : ℝ
hab : a ≤ b
δ_pos : 0 < δ
φ_cts : ∀ᶠ (z : ℂ) in 𝓝 z₀, ContinuousOn (φ z) (Icc a b)
φ_der : ∀ t ∈ Ioc a b, HasDerivAt (fun x => φ x t) (ψ t) z₀
φ_lip : ∀ t ∈ Ioc a b, LipschitzOnWith (nnabs C) (fun x => φ x t) (ball z₀ δ)
ψ_cts : ContinuousOn ψ (Ioc a b)
μ : Measure ℝ := Measure.restrict volume (Ioc a b)
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AEStronglyMeasurable (φ z) μ
h2 : Integrable (φ z₀) μ
h3 : AEStronglyMeasurable ψ μ
h4 : ∀ᵐ (t : ℝ) ∂μ, LipschitzOnWith (nnabs C) (fun z => φ z t) (ball z₀ δ)
h5 : Integrable (fun x => C) μ
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioc a b, φ z x ∂volume) (∫ (x : ℝ) in Ioc a b, ψ x ∂volume) z₀

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a✝ b✝ t : ℝ
n : ℕ
φ : ℂ → ℝ → ℂ
ψ : ℝ → ℂ
z₀ : ℂ
a b C δ : ℝ
hab : a ≤ b
δ_pos : 0 < δ
φ_cts : ∀ᶠ (z : ℂ) in 𝓝 z₀, ContinuousOn (φ z) (Icc a b)
φ_der : ∀ t ∈ Ioc a b, HasDerivAt (fun x => φ x t) (ψ t) z₀
φ_lip : ∀ t ∈ Ioc a b, LipschitzOnWith (nnabs C) (fun x => φ x t) (ball z₀ δ)
ψ_cts : ContinuousOn ψ (Ioc a b)
μ : Measure ℝ := Measure.restrict volume (Ioc a b)
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AEStronglyMeasurable (φ z) μ
h2 : Integrable (φ z₀) μ
h3 : AEStronglyMeasurable ψ μ
h4 : ∀ᵐ (t : ℝ) ∂μ, LipschitzOnWith (nnabs C) (fun z => φ z t) (ball z₀ δ)
h5 : Integrable (fun x => C) μ
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioc a b, φ z x ∂volume) (∫ (x : ℝ) in Ioc a b, ψ x ∂volume) z₀
Tactic:
have h6 : ∀ᵐ t ∂μ, HasDerivAt (λ z => φ z t) (ψ t) z₀ :=
  (ae_restrict_iff' measurableSet_Ioc).mpr (eventually_of_forall φ_der)
State after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a✝ b✝ t : ℝ
n : ℕ
φ : ℂ → ℝ → ℂ
ψ : ℝ → ℂ
z₀ : ℂ
a b C δ : ℝ
hab : a ≤ b
δ_pos : 0 < δ
φ_cts : ∀ᶠ (z : ℂ) in 𝓝 z₀, ContinuousOn (φ z) (Icc a b)
φ_der : ∀ t ∈ Ioc a b, HasDerivAt (fun x => φ x t) (ψ t) z₀
φ_lip : ∀ t ∈ Ioc a b, LipschitzOnWith (nnabs C) (fun x => φ x t) (ball z₀ δ)
ψ_cts : ContinuousOn ψ (Ioc a b)
μ : Measure ℝ := Measure.restrict volume (Ioc a b)
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AEStronglyMeasurable (φ z) μ
h2 : Integrable (φ z₀) μ
h3 : AEStronglyMeasurable ψ μ
h4 : ∀ᵐ (t : ℝ) ∂μ, LipschitzOnWith (nnabs C) (fun z => φ z t) (ball z₀ δ)
h5 : Integrable (fun x => C) μ
h6 : ∀ᵐ (t : ℝ) ∂μ, HasDerivAt (fun z => φ z t) (ψ t) z₀
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioc a b, φ z x ∂volume) (∫ (x : ℝ) in Ioc a b, ψ x ∂volume) z₀

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a✝ b✝ t : ℝ
n : ℕ
φ : ℂ → ℝ → ℂ
ψ : ℝ → ℂ
z₀ : ℂ
a b C δ : ℝ
hab : a ≤ b
δ_pos : 0 < δ
φ_cts : ∀ᶠ (z : ℂ) in 𝓝 z₀, ContinuousOn (φ z) (Icc a b)
φ_der : ∀ t ∈ Ioc a b, HasDerivAt (fun x => φ x t) (ψ t) z₀
φ_lip : ∀ t ∈ Ioc a b, LipschitzOnWith (nnabs C) (fun x => φ x t) (ball z₀ δ)
ψ_cts : ContinuousOn ψ (Ioc a b)
μ : Measure ℝ := Measure.restrict volume (Ioc a b)
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AEStronglyMeasurable (φ z) μ
h2 : Integrable (φ z₀) μ
h3 : AEStronglyMeasurable ψ μ
h4 : ∀ᵐ (t : ℝ) ∂μ, LipschitzOnWith (nnabs C) (fun z => φ z t) (ball z₀ δ)
h5 : Integrable (fun x => C) μ
h6 : ∀ᵐ (t : ℝ) ∂μ, HasDerivAt (fun z => φ z t) (ψ t) z₀
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioc a b, φ z x ∂volume) (∫ (x : ℝ) in Ioc a b, ψ x ∂volume) z₀
Tactic:
exact (hasDerivAt_integral_of_dominated_loc_of_lip δ_pos h1 h2 h3 h4 h5 h6).2
State after:
no goals