internlm/Lean-Github huggingface dataset:
Theorem: DifferentiableAt.deriv_eq_deriv_pow_div_pow
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ n : ℕ
n_pos : 0 < n
f g : ℂ → ℂ
hg : ∀ᶠ (z : ℂ) in 𝓝 z, f z = g z ^ n
g_diff : DifferentiableAt ℂ g z
fz_nonzero : f z ≠ 0
h1 : g z ≠ 0
h2 : ↑n * g z ^ (n - 1) ≠ 0
⊢ deriv g z = deriv f z / (↑n * g z ^ (n - 1))
Tactic:
rw [(EventuallyEq.deriv hg).self_of_nhds, deriv_pow'' _ g_diff, eq_div_iff h2]
Proof state after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ n : ℕ
n_pos : 0 < n
f g : ℂ → ℂ
hg : ∀ᶠ (z : ℂ) in 𝓝 z, f z = g z ^ n
g_diff : DifferentiableAt ℂ g z
fz_nonzero : f z ≠ 0
h1 : g z ≠ 0
h2 : ↑n * g z ^ (n - 1) ≠ 0
⊢ deriv g z * (↑n * g z ^ (n - 1)) = ↑n * g z ^ (n - 1) * deriv g z
Theorem: DifferentiableAt.deriv_eq_deriv_pow_div_pow
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ n : ℕ
n_pos : 0 < n
f g : ℂ → ℂ
hg : ∀ᶠ (z : ℂ) in 𝓝 z, f z = g z ^ n
g_diff : DifferentiableAt ℂ g z
fz_nonzero : f z ≠ 0
h1 : g z ≠ 0
h2 : ↑n * g z ^ (n - 1) ≠ 0
⊢ deriv g z * (↑n * g z ^ (n - 1)) = ↑n * g z ^ (n - 1) * deriv g z
Tactic:
ring
Proof state after:
no goals
Theorem: DifferentiableAt.deriv_eq_deriv_pow_div_pow
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ n : ℕ
n_pos : 0 < n
f g : ℂ → ℂ
hg : ∀ᶠ (z : ℂ) in 𝓝 z, f z = g z ^ n
g_diff : DifferentiableAt ℂ g z
fz_nonzero : f z ≠ 0
h : g z = 0
⊢ f z = 0
Tactic:
simp [Eventually.self_of_nhds hg, h, n_pos.ne.symm]
Proof state after:
no goals
Theorem: DifferentiableAt.deriv_eq_deriv_pow_div_pow
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ n : ℕ
n_pos : 0 < n
f g : ℂ → ℂ
hg : ∀ᶠ (z : ℂ) in 𝓝 z, f z = g z ^ n
g_diff : DifferentiableAt ℂ g z
fz_nonzero : f z ≠ 0
h1 : g z ≠ 0
⊢ ↑n * g z ^ (n - 1) ≠ 0
Tactic:
simp [pow_ne_zero, h1, n_pos.ne.symm]
Proof state after:
no goals
Theorem: has_deriv_at_integral_of_continuous_of_lip
Proof 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]
Proof 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₀
Theorem: has_deriv_at_integral_of_continuous_of_lip
Proof 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)
Proof 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₀
Theorem: has_deriv_at_integral_of_continuous_of_lip
Proof 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)
Proof 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₀
Theorem: has_deriv_at_integral_of_continuous_of_lip
Proof 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
Proof 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₀
Theorem: has_deriv_at_integral_of_continuous_of_lip
Proof 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
Proof 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₀
Theorem: has_deriv_at_integral_of_continuous_of_lip
Proof 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)
Proof 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₀
Theorem: has_deriv_at_integral_of_continuous_of_lip
Proof 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 _
Proof 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₀
Theorem: has_deriv_at_integral_of_continuous_of_lip
Proof 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)
Proof 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₀
Theorem: has_deriv_at_integral_of_continuous_of_lip
Proof 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
Proof state after:
no goals
Theorem: uIoo_eq_union
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
⊢ uIoo a b = Ioo a b ∪ Ioo b a
Tactic:
cases le_total a b <;> simp [*, uIoo]
Proof state after:
no goals
Theorem: mem_uIoo
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
⊢ t ∈ uIoo a b ↔ a < t ∧ t < b ∨ b < t ∧ t < a
Tactic:
simp [uIoo_eq_union]
Proof state after:
no goals
Theorem: uIoo_eq_uIoc_sdiff_ends
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
⊢ uIoo a b = Ι a b \ {a, b}
Tactic:
ext t
Proof state after:
case h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
⊢ t ∈ uIoo a b ↔ t ∈ Ι a b \ {a, b}
Theorem: uIoo_eq_uIoc_sdiff_ends
Proof state before:
case h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
⊢ t ∈ uIoo a b ↔ t ∈ Ι a b \ {a, b}
Tactic:
constructor <;> intro hh
Proof state after:
case h.mp
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : t ∈ uIoo a b
⊢ t ∈ Ι a b \ {a, b}

case h.mpr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : t ∈ Ι a b \ {a, b}
⊢ t ∈ uIoo a b
Theorem: uIoo_eq_uIoc_sdiff_ends
Proof state before:
case h.mp
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : t ∈ uIoo a b
⊢ t ∈ Ι a b \ {a, b}
Tactic:
simp [mem_uIoo] at hh
Proof state after:
case h.mp
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : a < t ∧ t < b ∨ b < t ∧ t < a
⊢ t ∈ Ι a b \ {a, b}
Theorem: uIoo_eq_uIoc_sdiff_ends
Proof state before:
case h.mp
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : a < t ∧ t < b ∨ b < t ∧ t < a
⊢ t ∈ Ι a b \ {a, b}
Tactic:
cases hh with
| inl h => simp [uIoc, h, h.2.le, h.1.ne.symm, h.2.ne]
| inr h => simp [uIoc, h, h.2.le, h.1.ne.symm, h.2.ne]
Proof state after:
no goals
Theorem: uIoo_eq_uIoc_sdiff_ends
Proof state before:
case h.mp.inl
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
h : a < t ∧ t < b
⊢ t ∈ Ι a b \ {a, b}
Tactic:
simp [uIoc, h, h.2.le, h.1.ne.symm, h.2.ne]
Proof state after:
no goals
Theorem: uIoo_eq_uIoc_sdiff_ends
Proof state before:
case h.mp.inr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
h : b < t ∧ t < a
⊢ t ∈ Ι a b \ {a, b}
Tactic:
simp [uIoc, h, h.2.le, h.1.ne.symm, h.2.ne]
Proof state after:
no goals
Theorem: uIoo_eq_uIoc_sdiff_ends
Proof state before:
case h.mpr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : t ∈ Ι a b \ {a, b}
⊢ t ∈ uIoo a b
Tactic:
simp_rw [uIoc, mem_diff, mem_Ioc, mem_insert_iff, mem_singleton_iff] at hh
Proof state after:
case h.mpr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : (min a b < t ∧ t ≤ max a b) ∧ ¬(t = a ∨ t = b)
⊢ t ∈ uIoo a b
Theorem: uIoo_eq_uIoc_sdiff_ends
Proof state before:
case h.mpr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : (min a b < t ∧ t ≤ max a b) ∧ ¬(t = a ∨ t = b)
⊢ t ∈ uIoo a b
Tactic:
push_neg at hh
Proof state after:
case h.mpr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : (min a b < t ∧ t ≤ max a b) ∧ t ≠ a ∧ t ≠ b
⊢ t ∈ uIoo a b
Theorem: uIoo_eq_uIoc_sdiff_ends
Proof state before:
case h.mpr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : (min a b < t ∧ t ≤ max a b) ∧ t ≠ a ∧ t ≠ b
⊢ t ∈ uIoo a b
Tactic:
refine ⟨hh.1.1, lt_of_le_of_ne hh.1.2 ?_⟩
Proof state after:
case h.mpr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : (min a b < t ∧ t ≤ max a b) ∧ t ≠ a ∧ t ≠ b
⊢ t ≠ a ⊔ b
Theorem: uIoo_eq_uIoc_sdiff_ends
Proof state before:
case h.mpr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : (min a b < t ∧ t ≤ max a b) ∧ t ≠ a ∧ t ≠ b
⊢ t ≠ a ⊔ b
Tactic:
cases le_total a b <;> simp [*]
Proof state after:
no goals
Theorem: uIoo_eq_uIcc_sdiff_ends
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
⊢ uIoo a b = uIcc a b \ {a, b}
Tactic:
cases le_total a b
Proof state after:
case inl
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
h✝ : a ≤ b
⊢ uIoo a b = uIcc a b \ {a, b}

case inr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
h✝ : b ≤ a
⊢ uIoo a b = uIcc a b \ {a, b}
Theorem: uIoo_eq_uIcc_sdiff_ends
Proof state before:
case inl
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
h✝ : a ≤ b
⊢ uIoo a b = uIcc a b \ {a, b}
Tactic:
simp [uIoo, uIcc, *]
Proof state after:
no goals
Theorem: uIoo_eq_uIcc_sdiff_ends
Proof state before:
case inr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
h✝ : b ≤ a
⊢ uIoo a b = uIcc a b \ {a, b}
Tactic:
simp [uIoo, uIcc, *, pair_comm a b]
Proof state after:
no goals
Theorem: uIoo_subset_uIcc
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
⊢ uIoo a b ⊆ uIcc a b
Tactic:
cases le_total a b <;> simp [uIoo, uIcc, Ioo_subset_Icc_self, *]
Proof state after:
no goals
Theorem: eventually_mem_uIoo_of_mem_uIoc
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
⊢ ∀ᵐ (x : ℝ), x ∈ Ι a b → x ∈ uIoo a b
Tactic:
apply eventually_of_mem (U := {a, b}ᶜ)
Proof state after:
case hU
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
⊢ {a, b}ᶜ ∈ Measure.ae volume

case h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
⊢ ∀ x ∈ {a, b}ᶜ, x ∈ Ι a b → x ∈ uIoo a b
Theorem: eventually_mem_uIoo_of_mem_uIoc
Proof state before:
case hU
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
⊢ {a, b}ᶜ ∈ Measure.ae volume
Tactic:
simpa only [mem_ae_iff, compl_compl] using measure_union_null volume_singleton volume_singleton
Proof state after:
no goals
Theorem: eventually_mem_uIoo_of_mem_uIoc
Proof state before:
case h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
⊢ ∀ x ∈ {a, b}ᶜ, x ∈ Ι a b → x ∈ uIoo a b
Tactic:
rw [uIoo_eq_uIoc_sdiff_ends]
Proof state after:
case h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
⊢ ∀ x ∈ {a, b}ᶜ, x ∈ Ι a b → x ∈ Ι a b \ {a, b}
Theorem: eventually_mem_uIoo_of_mem_uIoc
Proof state before:
case h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
⊢ ∀ x ∈ {a, b}ᶜ, x ∈ Ι a b → x ∈ Ι a b \ {a, b}
Tactic:
exact λ t h1 h2 => ⟨h2, h1⟩
Proof state after:
no goals
Theorem: derivWithin_of_mem_uIoo
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f✝ g f : ℝ → E
ht : t ∈ uIoo a b
⊢ derivWithin f (uIcc a b) t = deriv f t
Tactic:
rw [derivWithin, deriv, fderivWithin_of_mem_nhds (uIcc_mem_nhds ht)]
Proof state after:
no goals
Theorem: intervalIntegral.integral_congr_uIoo
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
h : EqOn f g (uIoo a b)
⊢ ∫ (t : ℝ) in a..b, f t = ∫ (t : ℝ) in a..b, g t
Tactic:
apply intervalIntegral.integral_congr_ae
Proof state after:
case h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
h : EqOn f g (uIoo a b)
⊢ ∀ᵐ (x : ℝ) ∂volume, x ∈ Ι a b → f x = g x
Theorem: intervalIntegral.integral_congr_uIoo
Proof state before:
case h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
h : EqOn f g (uIoo a b)
⊢ ∀ᵐ (x : ℝ) ∂volume, x ∈ Ι a b → f x = g x
Tactic:
filter_upwards [eventually_mem_uIoo_of_mem_uIoc] with t ht1 ht2 using h (ht1 ht2)
Proof state after:
no goals
Theorem: ContDiffOn.continuousOn_derivWithin''
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
n : ℕ∞
h : ContDiffOn ℝ n f (uIcc a b)
hn : 1 ≤ n
⊢ ContinuousOn (derivWithin f (uIcc a b)) (uIcc a b)
Tactic:
by_cases hab : a = b
Proof state after:
case pos
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
n : ℕ∞
h : ContDiffOn ℝ n f (uIcc a b)
hn : 1 ≤ n
hab : a = b
⊢ ContinuousOn (derivWithin f (uIcc a b)) (uIcc a b)

case neg
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
n : ℕ∞
h : ContDiffOn ℝ n f (uIcc a b)
hn : 1 ≤ n
hab : ¬a = b
⊢ ContinuousOn (derivWithin f (uIcc a b)) (uIcc a b)
Theorem: ContDiffOn.continuousOn_derivWithin''
Proof state before:
case pos
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
n : ℕ∞
h : ContDiffOn ℝ n f (uIcc a b)
hn : 1 ≤ n
hab : a = b
⊢ ContinuousOn (derivWithin f (uIcc a b)) (uIcc a b)
Tactic:
simp [continuousOn_singleton, hab]
Proof state after:
no goals
Theorem: ContDiffOn.continuousOn_derivWithin''
Proof state before:
case neg
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
n : ℕ∞
h : ContDiffOn ℝ n f (uIcc a b)
hn : 1 ≤ n
hab : ¬a = b
⊢ ContinuousOn (derivWithin f (uIcc a b)) (uIcc a b)
Tactic:
refine h.continuousOn_derivWithin (uniqueDiffOn_Icc (min_lt_max.2 hab)) hn
Proof state after:
no goals