internlm/Lean-Github huggingface dataset:
Theorem: integrable_iff_integrableAtFilter_atTop
Proof state before:
case mpr
X : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝² : LinearOrder X
inst✝¹ : OrderBot X
inst✝ : CompactIccSpace X
⊢ IntegrableAtFilter f atTop μ ∧ LocallyIntegrable f μ → Integrable f μ
Tactic:
refine fun h ↦ integrable_iff_integrableAtFilter_cocompact.mpr ⟨?_, h.2⟩
Proof state after:
case mpr
X : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝² : LinearOrder X
inst✝¹ : OrderBot X
inst✝ : CompactIccSpace X
h : IntegrableAtFilter f atTop μ ∧ LocallyIntegrable f μ
⊢ IntegrableAtFilter f (cocompact X) μ
Theorem: integrable_iff_integrableAtFilter_atTop
Proof state before:
case mpr
X : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝² : LinearOrder X
inst✝¹ : OrderBot X
inst✝ : CompactIccSpace X
h : IntegrableAtFilter f atTop μ ∧ LocallyIntegrable f μ
⊢ IntegrableAtFilter f (cocompact X) μ
Tactic:
exact h.1.filter_mono cocompact_le_atTop
Proof state after:
no goals
Theorem: integrableOn_Iic_iff_integrableAtFilter_atBot
Proof state before:
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
⊢ IntegrableOn f (Iic a) μ ↔ IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ
Tactic:
refine ⟨fun h ↦ ⟨⟨Iic a, Iic_mem_atBot a, h⟩, h.locallyIntegrableOn⟩, fun ⟨⟨s, hsl, hs⟩, h⟩ ↦ ?_⟩
Proof state after:
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ
s : Set X
hsl : s ∈ atBot
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Iic a) μ
⊢ IntegrableOn f (Iic a) μ
Theorem: integrableOn_Iic_iff_integrableAtFilter_atBot
Proof state before:
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ
s : Set X
hsl : s ∈ atBot
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Iic a) μ
⊢ IntegrableOn f (Iic a) μ
Tactic:
haveI : Nonempty X := Nonempty.intro a
Proof state after:
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ
s : Set X
hsl : s ∈ atBot
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Iic a) μ
this : Nonempty X
⊢ IntegrableOn f (Iic a) μ
Theorem: integrableOn_Iic_iff_integrableAtFilter_atBot
Proof state before:
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ
s : Set X
hsl : s ∈ atBot
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Iic a) μ
this : Nonempty X
⊢ IntegrableOn f (Iic a) μ
Tactic:
obtain ⟨a', ha'⟩ := mem_atBot_sets.mp hsl
Proof state after:
case intro
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ
s : Set X
hsl : s ∈ atBot
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Iic a) μ
this : Nonempty X
a' : X
ha' : ∀ b ≤ a', b ∈ s
⊢ IntegrableOn f (Iic a) μ
Theorem: integrableOn_Iic_iff_integrableAtFilter_atBot
Proof state before:
case intro
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ
s : Set X
hsl : s ∈ atBot
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Iic a) μ
this : Nonempty X
a' : X
ha' : ∀ b ≤ a', b ∈ s
⊢ IntegrableOn f (Iic a) μ
Tactic:
refine (integrableOn_union.mpr ⟨hs.mono ha' le_rfl, ?_⟩).mono Iic_subset_Iic_union_Icc le_rfl
Proof state after:
case intro
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ
s : Set X
hsl : s ∈ atBot
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Iic a) μ
this : Nonempty X
a' : X
ha' : ∀ b ≤ a', b ∈ s
⊢ IntegrableOn f (Icc a' a) μ
Theorem: integrableOn_Iic_iff_integrableAtFilter_atBot
Proof state before:
case intro
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ
s : Set X
hsl : s ∈ atBot
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Iic a) μ
this : Nonempty X
a' : X
ha' : ∀ b ≤ a', b ∈ s
⊢ IntegrableOn f (Icc a' a) μ
Tactic:
exact h.integrableOn_compact_subset Icc_subset_Iic_self isCompact_Icc
Proof state after:
no goals
Theorem: integrableOn_Ici_iff_integrableAtFilter_atTop
Proof state before:
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
⊢ IntegrableOn f (Ici a) μ ↔ IntegrableAtFilter f atTop μ ∧ LocallyIntegrableOn f (Ici a) μ
Tactic:
refine ⟨fun h ↦ ⟨⟨Ici a, Ici_mem_atTop a, h⟩, h.locallyIntegrableOn⟩, fun ⟨⟨s, hsl, hs⟩, h⟩ ↦ ?_⟩
Proof state after:
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atTop μ ∧ LocallyIntegrableOn f (Ici a) μ
s : Set X
hsl : s ∈ atTop
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Ici a) μ
⊢ IntegrableOn f (Ici a) μ
Theorem: integrableOn_Ici_iff_integrableAtFilter_atTop
Proof state before:
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atTop μ ∧ LocallyIntegrableOn f (Ici a) μ
s : Set X
hsl : s ∈ atTop
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Ici a) μ
⊢ IntegrableOn f (Ici a) μ
Tactic:
haveI : Nonempty X := Nonempty.intro a
Proof state after:
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atTop μ ∧ LocallyIntegrableOn f (Ici a) μ
s : Set X
hsl : s ∈ atTop
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Ici a) μ
this : Nonempty X
⊢ IntegrableOn f (Ici a) μ
Theorem: integrableOn_Ici_iff_integrableAtFilter_atTop
Proof state before:
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atTop μ ∧ LocallyIntegrableOn f (Ici a) μ
s : Set X
hsl : s ∈ atTop
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Ici a) μ
this : Nonempty X
⊢ IntegrableOn f (Ici a) μ
Tactic:
obtain ⟨a', ha'⟩ := mem_atTop_sets.mp hsl
Proof state after:
case intro
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atTop μ ∧ LocallyIntegrableOn f (Ici a) μ
s : Set X
hsl : s ∈ atTop
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Ici a) μ
this : Nonempty X
a' : X
ha' : ∀ b ≥ a', b ∈ s
⊢ IntegrableOn f (Ici a) μ
Theorem: integrableOn_Ici_iff_integrableAtFilter_atTop
Proof state before:
case intro
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atTop μ ∧ LocallyIntegrableOn f (Ici a) μ
s : Set X
hsl : s ∈ atTop
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Ici a) μ
this : Nonempty X
a' : X
ha' : ∀ b ≥ a', b ∈ s
⊢ IntegrableOn f (Ici a) μ
Tactic:
refine (integrableOn_union.mpr ⟨?_, hs.mono ha' le_rfl⟩).mono Ici_subset_Icc_union_Ici le_rfl
Proof state after:
case intro
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atTop μ ∧ LocallyIntegrableOn f (Ici a) μ
s : Set X
hsl : s ∈ atTop
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Ici a) μ
this : Nonempty X
a' : X
ha' : ∀ b ≥ a', b ∈ s
⊢ IntegrableOn f (Icc a a') μ
Theorem: integrableOn_Ici_iff_integrableAtFilter_atTop
Proof state before:
case intro
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atTop μ ∧ LocallyIntegrableOn f (Ici a) μ
s : Set X
hsl : s ∈ atTop
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Ici a) μ
this : Nonempty X
a' : X
ha' : ∀ b ≥ a', b ∈ s
⊢ IntegrableOn f (Icc a a') μ
Tactic:
exact h.integrableOn_compact_subset Icc_subset_Ici_self isCompact_Icc
Proof state after:
no goals
Theorem: div_cpow_eq_cpow_neg
Proof state before:
a x s : ℂ
⊢ a / x ^ s = a * x ^ (-s)
Tactic:
rw [div_eq_mul_inv, cpow_neg]
Proof state after:
no goals
Theorem: one_div_cpow_eq_cpow_neg
Proof state before:
x s : ℂ
⊢ 1 / x ^ s = x ^ (-s)
Tactic:
convert div_cpow_eq_cpow_neg 1 x s using 1
Proof state after:
case h.e'_3
x s : ℂ
⊢ x ^ (-s) = 1 * x ^ (-s)
Theorem: one_div_cpow_eq_cpow_neg
Proof state before:
case h.e'_3
x s : ℂ
⊢ x ^ (-s) = 1 * x ^ (-s)
Tactic:
simp
Proof state after:
no goals
Theorem: div_rpow_eq_rpow_neg
Proof state before:
a x s : ℝ
hx : 0 ≤ x
⊢ a / x ^ s = a * x ^ (-s)
Tactic:
rw [div_eq_mul_inv, Real.rpow_neg hx]
Proof state after:
no goals
Theorem: div_rpow_neg_eq_rpow_div
Proof state before:
x y s : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ x ^ (-s) / y ^ (-s) = (y / x) ^ s
Tactic:
rw [div_eq_mul_inv, Real.rpow_neg hx, Real.rpow_neg hy, Real.div_rpow hy hx]
Proof state after:
x y s : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ (x ^ s)⁻¹ * (y ^ s)⁻¹⁻¹ = y ^ s / x ^ s
Theorem: div_rpow_neg_eq_rpow_div
Proof state before:
x y s : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ (x ^ s)⁻¹ * (y ^ s)⁻¹⁻¹ = y ^ s / x ^ s
Tactic:
field_simp
Proof state after:
no goals
Theorem: div_rpow_eq_rpow_div_neg
Proof state before:
x y s : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ x ^ s / y ^ s = (y / x) ^ (-s)
Tactic:
convert div_rpow_neg_eq_rpow_div (s := -s) hx hy using 1
Proof state after:
case h.e'_2
x y s : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ x ^ s / y ^ s = x ^ (- -s) / y ^ (- -s)
Theorem: div_rpow_eq_rpow_div_neg
Proof state before:
case h.e'_2
x y s : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ x ^ s / y ^ s = x ^ (- -s) / y ^ (- -s)
Tactic:
simp only [neg_neg]
Proof state after:
no goals
Theorem: riemannZeta0_apply
Proof state before:
N : ℕ
s : ℂ
⊢ ζ₀ N s =
    ∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ s +
      (-↑N ^ (1 - s) / (1 - s) + -↑N ^ (-s) / 2 + s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)))
Tactic:
simp_rw [riemannZeta0, div_cpow_eq_cpow_neg]
Proof state after:
N : ℕ
s : ℂ
⊢ ∑ x ∈ Finset.range (N + 1), 1 * ↑x ^ (-s) + -↑N ^ (1 - s) / (1 - s) + -↑N ^ (-s) / 2 +
      s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)) =
    ∑ x ∈ Finset.range (N + 1), 1 * ↑x ^ (-s) +
      (-↑N ^ (1 - s) / (1 - s) + -↑N ^ (-s) / 2 + s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)))
Theorem: riemannZeta0_apply
Proof state before:
N : ℕ
s : ℂ
⊢ ∑ x ∈ Finset.range (N + 1), 1 * ↑x ^ (-s) + -↑N ^ (1 - s) / (1 - s) + -↑N ^ (-s) / 2 +
      s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)) =
    ∑ x ∈ Finset.range (N + 1), 1 * ↑x ^ (-s) +
      (-↑N ^ (1 - s) / (1 - s) + -↑N ^ (-s) / 2 + s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)))
Tactic:
ring
Proof state after:
no goals
Theorem: Real.differentiableAt_cpow_const_of_ne
Proof state before:
s : ℂ
x : ℝ
xpos : 0 < x
⊢ DifferentiableAt ℝ (fun x => ↑x ^ s) x
Tactic:
apply DifferentiableAt.comp_ofReal (e := fun z ↦ z ^ s)
Proof state after:
s : ℂ
x : ℝ
xpos : 0 < x
⊢ DifferentiableAt ℂ (fun z => z ^ s) ↑x
Theorem: Real.differentiableAt_cpow_const_of_ne
Proof state before:
s : ℂ
x : ℝ
xpos : 0 < x
⊢ DifferentiableAt ℂ (fun z => z ^ s) ↑x
Tactic:
apply DifferentiableAt.cpow (by simp) (by simp) (by simp [xpos])
Proof state after:
no goals
Theorem: Real.differentiableAt_cpow_const_of_ne
Proof state before:
s : ℂ
x : ℝ
xpos : 0 < x
⊢ DifferentiableAt ℂ (fun x => x) ↑x
Tactic:
simp
Proof state after:
no goals
Theorem: Real.differentiableAt_cpow_const_of_ne
Proof state before:
s : ℂ
x : ℝ
xpos : 0 < x
⊢ DifferentiableAt ℂ (fun x => s) ↑x
Tactic:
simp
Proof state after:
no goals
Theorem: Real.differentiableAt_cpow_const_of_ne
Proof state before:
s : ℂ
x : ℝ
xpos : 0 < x
⊢ ↑x ∈ slitPlane
Tactic:
simp [xpos]
Proof state after:
no goals
Theorem: Complex.one_div_cpow_eq
Proof state before:
s : ℂ
x : ℝ
x_ne : x ≠ 0
⊢ 1 / ↑x ^ s = ↑x ^ (-s)
Tactic:
refine (eq_one_div_of_mul_eq_one_left ?_).symm
Proof state after:
s : ℂ
x : ℝ
x_ne : x ≠ 0
⊢ ↑x ^ (-s) * ↑x ^ s = 1
Theorem: Complex.one_div_cpow_eq
Proof state before:
s : ℂ
x : ℝ
x_ne : x ≠ 0
⊢ ↑x ^ (-s) * ↑x ^ s = 1
Tactic:
rw [← cpow_add _ _ <| mod_cast x_ne, add_left_neg, cpow_zero]
Proof state after:
no goals
Theorem: ContDiffOn.hasDeriv_deriv
Proof state before:
φ : ℝ → ℂ
s : Set ℝ
φDiff : ContDiffOn ℝ 1 φ s
x : ℝ
x_in_s : s ∈ 𝓝 x
⊢ 1 ≤ 1
Tactic:
simp
Proof state after:
no goals
Theorem: ContDiffOn.continuousOn_deriv
Proof state before:
φ : ℝ → ℂ
a b : ℝ
φDiff : ContDiffOn ℝ 1 φ (uIoo a b)
⊢ ContinuousOn (deriv φ) (uIoo a b)
Tactic:
apply ContDiffOn.continuousOn (𝕜 := ℝ) (n := 0)
Proof state after:
φ : ℝ → ℂ
a b : ℝ
φDiff : ContDiffOn ℝ 1 φ (uIoo a b)
⊢ ContDiffOn ℝ 0 (deriv φ) (uIoo a b)
Theorem: ContDiffOn.continuousOn_deriv
Proof state before:
φ : ℝ → ℂ
a b : ℝ
φDiff : ContDiffOn ℝ 1 φ (uIoo a b)
⊢ ContDiffOn ℝ 0 (deriv φ) (uIoo a b)
Tactic:
exact (fun h ↦ ((contDiffOn_succ_iff_deriv_of_isOpen isOpen_Ioo).1 h).2) φDiff
Proof state after:
no goals
Theorem: LinearDerivative_ofReal
Proof state before:
x : ℝ
a b : ℂ
⊢ HasDerivAt (fun t => a * ↑t + b) a x
Tactic:
refine HasDerivAt.add_const ?_ b
Proof state after:
x : ℝ
a b : ℂ
⊢ HasDerivAt (fun t => a * ↑t) a x
Theorem: LinearDerivative_ofReal
Proof state before:
x : ℝ
a b : ℂ
⊢ HasDerivAt (fun t => a * ↑t) a x
Tactic:
convert (ContinuousLinearMap.hasDerivAt Complex.ofRealCLM).const_mul a using 1
Proof state after:
case h.e'_7
x : ℝ
a b : ℂ
⊢ a = a * ofRealCLM 1
Theorem: LinearDerivative_ofReal
Proof state before:
case h.e'_7
x : ℝ
a b : ℂ
⊢ a = a * ofRealCLM 1
Tactic:
simp
Proof state after:
no goals
Theorem: integral_deriv_mul_eq_sub'
Proof state before:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a b : ℝ
u v u' v' : ℝ → A
hu : ∀ x ∈ [[a, b]], HasDerivWithinAt u (u' x) [[a, b]] x
hv : ∀ x ∈ [[a, b]], HasDerivWithinAt v (v' x) [[a, b]] x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ ∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a
Tactic:
have h2u : ContinuousOn u [[a, b]] := fun x hx ↦ (hu x hx).continuousWithinAt
Proof state after:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a b : ℝ
u v u' v' : ℝ → A
hu : ∀ x ∈ [[a, b]], HasDerivWithinAt u (u' x) [[a, b]] x
hv : ∀ x ∈ [[a, b]], HasDerivWithinAt v (v' x) [[a, b]] x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
h2u : ContinuousOn u [[a, b]]
⊢ ∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a
Theorem: integral_deriv_mul_eq_sub'
Proof state before:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a b : ℝ
u v u' v' : ℝ → A
hu : ∀ x ∈ [[a, b]], HasDerivWithinAt u (u' x) [[a, b]] x
hv : ∀ x ∈ [[a, b]], HasDerivWithinAt v (v' x) [[a, b]] x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
h2u : ContinuousOn u [[a, b]]
⊢ ∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a
Tactic:
have h2v : ContinuousOn v [[a, b]] := fun x hx ↦ (hv x hx).continuousWithinAt
Proof state after:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a b : ℝ
u v u' v' : ℝ → A
hu : ∀ x ∈ [[a, b]], HasDerivWithinAt u (u' x) [[a, b]] x
hv : ∀ x ∈ [[a, b]], HasDerivWithinAt v (v' x) [[a, b]] x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
h2u : ContinuousOn u [[a, b]]
h2v : ContinuousOn v [[a, b]]
⊢ ∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a
Theorem: integral_deriv_mul_eq_sub'
Proof state before:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a b : ℝ
u v u' v' : ℝ → A
hu : ∀ x ∈ [[a, b]], HasDerivWithinAt u (u' x) [[a, b]] x
hv : ∀ x ∈ [[a, b]], HasDerivWithinAt v (v' x) [[a, b]] x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
h2u : ContinuousOn u [[a, b]]
h2v : ContinuousOn v [[a, b]]
⊢ ∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a
Tactic:
apply integral_eq_sub_of_hasDeriv_right (h2u.mul h2v)
Proof state after:
case hderiv
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a b : ℝ
u v u' v' : ℝ → A
hu : ∀ x ∈ [[a, b]], HasDerivWithinAt u (u' x) [[a, b]] x
hv : ∀ x ∈ [[a, b]], HasDerivWithinAt v (v' x) [[a, b]] x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
h2u : ContinuousOn u [[a, b]]
h2v : ContinuousOn v [[a, b]]
⊢ ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt (fun x => u x * v x) (u' x * v x + u x * v' x) (Ioi x) x

case hint
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a b : ℝ
u v u' v' : ℝ → A
hu : ∀ x ∈ [[a, b]], HasDerivWithinAt u (u' x) [[a, b]] x
hv : ∀ x ∈ [[a, b]], HasDerivWithinAt v (v' x) [[a, b]] x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
h2u : ContinuousOn u [[a, b]]
h2v : ContinuousOn v [[a, b]]
⊢ IntervalIntegrable (fun y => u' y * v y + u y * v' y) volume a b
Theorem: integral_deriv_mul_eq_sub'
Proof state before:
case hderiv
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a b : ℝ
u v u' v' : ℝ → A
hu : ∀ x ∈ [[a, b]], HasDerivWithinAt u (u' x) [[a, b]] x
hv : ∀ x ∈ [[a, b]], HasDerivWithinAt v (v' x) [[a, b]] x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
h2u : ContinuousOn u [[a, b]]
h2v : ContinuousOn v [[a, b]]
⊢ ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt (fun x => u x * v x) (u' x * v x + u x * v' x) (Ioi x) x
Tactic:
exact fun x hx ↦ (hu x <| mem_Icc_of_Ioo hx).mul (hv x <| mem_Icc_of_Ioo hx) |>.hasDerivAt
  (Icc_mem_nhds hx.1 hx.2) |>.hasDerivWithinAt
Proof state after:
no goals
Theorem: integral_deriv_mul_eq_sub'
Proof state before:
case hint
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a b : ℝ
u v u' v' : ℝ → A
hu : ∀ x ∈ [[a, b]], HasDerivWithinAt u (u' x) [[a, b]] x
hv : ∀ x ∈ [[a, b]], HasDerivWithinAt v (v' x) [[a, b]] x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
h2u : ContinuousOn u [[a, b]]
h2v : ContinuousOn v [[a, b]]
⊢ IntervalIntegrable (fun y => u' y * v y + u y * v' y) volume a b
Tactic:
exact (hu'.mul_continuousOn h2v).add (hv'.continuousOn_mul h2u)
Proof state after:
no goals
Theorem: sum_eq_int_deriv_aux2
Proof state before:
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
⊢ ∫ (x : ℝ) in a..b, (c - ↑x) * deriv φ x = (c - ↑b) * φ b - (c - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x
Tactic:
set u := fun (x : ℝ) ↦ c - x
Proof state after:
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
u : ℝ → ℂ := fun x => c - ↑x
⊢ ∫ (x : ℝ) in a..b, (c - ↑x) * deriv φ x = (c - ↑b) * φ b - (c - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x
Theorem: sum_eq_int_deriv_aux2
Proof state before:
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
u : ℝ → ℂ := fun x => c - ↑x
⊢ ∫ (x : ℝ) in a..b, (c - ↑x) * deriv φ x = (c - ↑b) * φ b - (c - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x
Tactic:
set u' := fun (x : ℝ) ↦ (-1 : ℂ)
Proof state after:
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
u : ℝ → ℂ := fun x => c - ↑x
u' : ℝ → ℂ := fun x => -1
⊢ ∫ (x : ℝ) in a..b, (c - ↑x) * deriv φ x = (c - ↑b) * φ b - (c - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x
Theorem: sum_eq_int_deriv_aux2
Proof state before:
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
u : ℝ → ℂ := fun x => c - ↑x
u' : ℝ → ℂ := fun x => -1
⊢ ∫ (x : ℝ) in a..b, (c - ↑x) * deriv φ x = (c - ↑b) * φ b - (c - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x
Tactic:
have hu : ∀ x ∈ uIcc a b, HasDerivAt u (u' x) x := by
  exact fun x _ ↦ by convert LinearDerivative_ofReal x (-1 : ℂ) c; ring
Proof state after:
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
u : ℝ → ℂ := fun x => c - ↑x
u' : ℝ → ℂ := fun x => -1
hu : ∀ x ∈ [[a, b]], HasDerivAt u (u' x) x
⊢ ∫ (x : ℝ) in a..b, (c - ↑x) * deriv φ x = (c - ↑b) * φ b - (c - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x
Theorem: sum_eq_int_deriv_aux2
Proof state before:
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
u : ℝ → ℂ := fun x => c - ↑x
u' : ℝ → ℂ := fun x => -1
hu : ∀ x ∈ [[a, b]], HasDerivAt u (u' x) x
⊢ ∫ (x : ℝ) in a..b, (c - ↑x) * deriv φ x = (c - ↑b) * φ b - (c - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x
Tactic:
have hu' : IntervalIntegrable u' MeasureTheory.volume a b := by
  apply Continuous.intervalIntegrable; continuity
Proof state after:
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
u : ℝ → ℂ := fun x => c - ↑x
u' : ℝ → ℂ := fun x => -1
hu : ∀ x ∈ [[a, b]], HasDerivAt u (u' x) x
hu' : IntervalIntegrable u' MeasureTheory.volume a b
⊢ ∫ (x : ℝ) in a..b, (c - ↑x) * deriv φ x = (c - ↑b) * φ b - (c - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x
Theorem: sum_eq_int_deriv_aux2
Proof state before:
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
u : ℝ → ℂ := fun x => c - ↑x
u' : ℝ → ℂ := fun x => -1
hu : ∀ x ∈ [[a, b]], HasDerivAt u (u' x) x
hu' : IntervalIntegrable u' MeasureTheory.volume a b
⊢ ∫ (x : ℝ) in a..b, (c - ↑x) * deriv φ x = (c - ↑b) * φ b - (c - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x
Tactic:
have hv' : IntervalIntegrable (deriv φ) MeasureTheory.volume a b :=
  derivφCont.intervalIntegrable
Proof state after:
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
u : ℝ → ℂ := fun x => c - ↑x
u' : ℝ → ℂ := fun x => -1
hu : ∀ x ∈ [[a, b]], HasDerivAt u (u' x) x
hu' : IntervalIntegrable u' MeasureTheory.volume a b
hv' : IntervalIntegrable (deriv φ) MeasureTheory.volume a b
⊢ ∫ (x : ℝ) in a..b, (c - ↑x) * deriv φ x = (c - ↑b) * φ b - (c - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x