internlm/Lean-Github huggingface dataset:
Theorem: DifferentiableAt.ofReal_comp_iff
Proof state before:
case intro.intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
H : DifferentiableAt ℝ (fun y => ↑(f y)) z
u : ℝ
left✝ : deriv (fun y => ↑(f y)) z = ↑u
hu₂ : HasDerivAt (fun y => f y) u z
⊢ DifferentiableAt ℝ f z
Tactic:
exact HasDerivAt.differentiableAt hu₂
Proof state after:
no goals
Theorem: deriv.ofReal_comp
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
⊢ deriv (fun y => ↑(f y)) z = ↑(deriv f z)
Tactic:
by_cases hf : DifferentiableAt ℝ f z
Proof state after:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
hf : DifferentiableAt ℝ f z
⊢ deriv (fun y => ↑(f y)) z = ↑(deriv f z)

case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
hf : ¬DifferentiableAt ℝ f z
⊢ deriv (fun y => ↑(f y)) z = ↑(deriv f z)
Theorem: deriv.ofReal_comp
Proof state before:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
hf : DifferentiableAt ℝ f z
⊢ deriv (fun y => ↑(f y)) z = ↑(deriv f z)
Tactic:
exact hf.hasDerivAt.ofReal_comp.deriv
Proof state after:
no goals
Theorem: deriv.ofReal_comp
Proof state before:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
hf : ¬DifferentiableAt ℝ f z
⊢ deriv (fun y => ↑(f y)) z = ↑(deriv f z)
Tactic:
have hf' := mt DifferentiableAt.ofReal_comp_iff.mp hf
Proof state after:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
hf : ¬DifferentiableAt ℝ f z
hf' : ¬DifferentiableAt ℝ (fun y => ↑(f y)) z
⊢ deriv (fun y => ↑(f y)) z = ↑(deriv f z)
Theorem: deriv.ofReal_comp
Proof state before:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
hf : ¬DifferentiableAt ℝ f z
hf' : ¬DifferentiableAt ℝ (fun y => ↑(f y)) z
⊢ deriv (fun y => ↑(f y)) z = ↑(deriv f z)
Tactic:
rw [deriv_zero_of_not_differentiableAt hf, deriv_zero_of_not_differentiableAt <| hf',
  Complex.ofReal_zero]
Proof state after:
no goals
Theorem: PartialIntegration
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
fDiff : DifferentiableOn ℝ f (Ioi 0)
gDiff : DifferentiableOn ℝ g (Ioi 0)
fDerivgInt : IntegrableOn (f * deriv g) (Ioi 0) volume
gDerivfInt : IntegrableOn (deriv f * g) (Ioi 0) volume
lim_at_zero : Tendsto (f * g) (𝓝[>] 0) (𝓝 0)
lim_at_inf : Tendsto (f * g) atTop (𝓝 0)
⊢ ∫ (x : ℝ) in Ioi 0, f x * deriv g x = -∫ (x : ℝ) in Ioi 0, deriv f x * g x
Tactic:
simpa using integral_Ioi_mul_deriv_eq_deriv_mul
  (fun x hx ↦ fDiff.hasDerivAt (Ioi_mem_nhds hx))
  (fun x hx ↦ gDiff.hasDerivAt (Ioi_mem_nhds hx))
  fDerivgInt gDerivfInt lim_at_zero lim_at_inf
Proof state after:
no goals
Theorem: PartialIntegration_of_support_in_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f g : ℝ → ℂ
ha : 0 < a
h : a ≤ b
fSupp : Function.support f ⊆ Icc a b
fDiff : DifferentiableOn ℝ f (Ioi 0)
gDiff : DifferentiableOn ℝ g (Ioi 0)
fderivCont : ContinuousOn (deriv f) (Ioi 0)
gderivCont : ContinuousOn (deriv g) (Ioi 0)
⊢ ∫ (x : ℝ) in Ioi 0, f x * deriv g x = -∫ (x : ℝ) in Ioi 0, deriv f x * g x
Tactic:
have Icc_sub : Icc a b ⊆ Ioi 0 := (Icc_subset_Ioi_iff h).mpr ha
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f g : ℝ → ℂ
ha : 0 < a
h : a ≤ b
fSupp : Function.support f ⊆ Icc a b
fDiff : DifferentiableOn ℝ f (Ioi 0)
gDiff : DifferentiableOn ℝ g (Ioi 0)
fderivCont : ContinuousOn (deriv f) (Ioi 0)
gderivCont : ContinuousOn (deriv g) (Ioi 0)
Icc_sub : Icc a b ⊆ Ioi 0
⊢ ∫ (x : ℝ) in Ioi 0, f x * deriv g x = -∫ (x : ℝ) in Ioi 0, deriv f x * g x
Theorem: PartialIntegration_of_support_in_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f g : ℝ → ℂ
ha : 0 < a
h : a ≤ b
fSupp : Function.support f ⊆ Icc a b
fDiff : DifferentiableOn ℝ f (Ioi 0)
gDiff : DifferentiableOn ℝ g (Ioi 0)
fderivCont : ContinuousOn (deriv f) (Ioi 0)
gderivCont : ContinuousOn (deriv g) (Ioi 0)
Icc_sub : Icc a b ⊆ Ioi 0
⊢ ∫ (x : ℝ) in Ioi 0, f x * deriv g x = -∫ (x : ℝ) in Ioi 0, deriv f x * g x
Tactic:
have fderivSupp := Function.support_deriv_subset_Icc fSupp
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f g : ℝ → ℂ
ha : 0 < a
h : a ≤ b
fSupp : Function.support f ⊆ Icc a b
fDiff : DifferentiableOn ℝ f (Ioi 0)
gDiff : DifferentiableOn ℝ g (Ioi 0)
fderivCont : ContinuousOn (deriv f) (Ioi 0)
gderivCont : ContinuousOn (deriv g) (Ioi 0)
Icc_sub : Icc a b ⊆ Ioi 0
fderivSupp : Function.support (deriv f) ⊆ Icc a b
⊢ ∫ (x : ℝ) in Ioi 0, f x * deriv g x = -∫ (x : ℝ) in Ioi 0, deriv f x * g x
Theorem: PartialIntegration_of_support_in_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f g : ℝ → ℂ
ha : 0 < a
h : a ≤ b
fSupp : Function.support f ⊆ Icc a b
fDiff : DifferentiableOn ℝ f (Ioi 0)
gDiff : DifferentiableOn ℝ g (Ioi 0)
fderivCont : ContinuousOn (deriv f) (Ioi 0)
gderivCont : ContinuousOn (deriv g) (Ioi 0)
Icc_sub : Icc a b ⊆ Ioi 0
fderivSupp : Function.support (deriv f) ⊆ Icc a b
⊢ ∫ (x : ℝ) in Ioi 0, f x * deriv g x = -∫ (x : ℝ) in Ioi 0, deriv f x * g x
Tactic:
have fgSupp : (f * g).support ⊆ Icc a b := Function.support_mul_subset_of_subset fSupp
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f g : ℝ → ℂ
ha : 0 < a
h : a ≤ b
fSupp : Function.support f ⊆ Icc a b
fDiff : DifferentiableOn ℝ f (Ioi 0)
gDiff : DifferentiableOn ℝ g (Ioi 0)
fderivCont : ContinuousOn (deriv f) (Ioi 0)
gderivCont : ContinuousOn (deriv g) (Ioi 0)
Icc_sub : Icc a b ⊆ Ioi 0
fderivSupp : Function.support (deriv f) ⊆ Icc a b
fgSupp : Function.support (f * g) ⊆ Icc a b
⊢ ∫ (x : ℝ) in Ioi 0, f x * deriv g x = -∫ (x : ℝ) in Ioi 0, deriv f x * g x
Theorem: PartialIntegration_of_support_in_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f g : ℝ → ℂ
ha : 0 < a
h : a ≤ b
fSupp : Function.support f ⊆ Icc a b
fDiff : DifferentiableOn ℝ f (Ioi 0)
gDiff : DifferentiableOn ℝ g (Ioi 0)
fderivCont : ContinuousOn (deriv f) (Ioi 0)
gderivCont : ContinuousOn (deriv g) (Ioi 0)
Icc_sub : Icc a b ⊆ Ioi 0
fderivSupp : Function.support (deriv f) ⊆ Icc a b
fgSupp : Function.support (f * g) ⊆ Icc a b
⊢ ∫ (x : ℝ) in Ioi 0, f x * deriv g x = -∫ (x : ℝ) in Ioi 0, deriv f x * g x
Tactic:
have fDerivgInt : IntegrableOn (f * deriv g) (Ioi 0) := by
  apply (integrableOn_iff_integrable_of_support_subset <|
         Function.support_mul_subset_of_subset fSupp).mp
  exact fDiff.continuousOn.mono Icc_sub |>.mul (gderivCont.mono Icc_sub) |>.integrableOn_Icc
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f g : ℝ → ℂ
ha : 0 < a
h : a ≤ b
fSupp : Function.support f ⊆ Icc a b
fDiff : DifferentiableOn ℝ f (Ioi 0)
gDiff : DifferentiableOn ℝ g (Ioi 0)
fderivCont : ContinuousOn (deriv f) (Ioi 0)
gderivCont : ContinuousOn (deriv g) (Ioi 0)
Icc_sub : Icc a b ⊆ Ioi 0
fderivSupp : Function.support (deriv f) ⊆ Icc a b
fgSupp : Function.support (f * g) ⊆ Icc a b
fDerivgInt : IntegrableOn (f * deriv g) (Ioi 0) volume
⊢ ∫ (x : ℝ) in Ioi 0, f x * deriv g x = -∫ (x : ℝ) in Ioi 0, deriv f x * g x
Theorem: PartialIntegration_of_support_in_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f g : ℝ → ℂ
ha : 0 < a
h : a ≤ b
fSupp : Function.support f ⊆ Icc a b
fDiff : DifferentiableOn ℝ f (Ioi 0)
gDiff : DifferentiableOn ℝ g (Ioi 0)
fderivCont : ContinuousOn (deriv f) (Ioi 0)
gderivCont : ContinuousOn (deriv g) (Ioi 0)
Icc_sub : Icc a b ⊆ Ioi 0
fderivSupp : Function.support (deriv f) ⊆ Icc a b
fgSupp : Function.support (f * g) ⊆ Icc a b
fDerivgInt : IntegrableOn (f * deriv g) (Ioi 0) volume
⊢ ∫ (x : ℝ) in Ioi 0, f x * deriv g x = -∫ (x : ℝ) in Ioi 0, deriv f x * g x
Tactic:
have gDerivfInt : IntegrableOn (deriv f * g) (Ioi 0) := by
  apply (integrableOn_iff_integrable_of_support_subset <|
         Function.support_mul_subset_of_subset fderivSupp).mp
  exact fderivCont.mono Icc_sub |>.mul (gDiff.continuousOn.mono Icc_sub) |>.integrableOn_Icc
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f g : ℝ → ℂ
ha : 0 < a
h : a ≤ b
fSupp : Function.support f ⊆ Icc a b
fDiff : DifferentiableOn ℝ f (Ioi 0)
gDiff : DifferentiableOn ℝ g (Ioi 0)
fderivCont : ContinuousOn (deriv f) (Ioi 0)
gderivCont : ContinuousOn (deriv g) (Ioi 0)
Icc_sub : Icc a b ⊆ Ioi 0
fderivSupp : Function.support (deriv f) ⊆ Icc a b
fgSupp : Function.support (f * g) ⊆ Icc a b
fDerivgInt : IntegrableOn (f * deriv g) (Ioi 0) volume
gDerivfInt : IntegrableOn (deriv f * g) (Ioi 0) volume
⊢ ∫ (x : ℝ) in Ioi 0, f x * deriv g x = -∫ (x : ℝ) in Ioi 0, deriv f x * g x
Theorem: PartialIntegration_of_support_in_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f g : ℝ → ℂ
ha : 0 < a
h : a ≤ b
fSupp : Function.support f ⊆ Icc a b
fDiff : DifferentiableOn ℝ f (Ioi 0)
gDiff : DifferentiableOn ℝ g (Ioi 0)
fderivCont : ContinuousOn (deriv f) (Ioi 0)
gderivCont : ContinuousOn (deriv g) (Ioi 0)
Icc_sub : Icc a b ⊆ Ioi 0
fderivSupp : Function.support (deriv f) ⊆ Icc a b
fgSupp : Function.support (f * g) ⊆ Icc a b
fDerivgInt : IntegrableOn (f * deriv g) (Ioi 0) volume
gDerivfInt : IntegrableOn (deriv f * g) (Ioi 0) volume
⊢ ∫ (x : ℝ) in Ioi 0, f x * deriv g x = -∫ (x : ℝ) in Ioi 0, deriv f x * g x
Tactic:
have lim_at_zero : Tendsto (f * g) (𝓝[>]0) (𝓝 0) := TendstoAtZero_of_support_in_Icc (f * g) ha fgSupp
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f g : ℝ → ℂ
ha : 0 < a
h : a ≤ b
fSupp : Function.support f ⊆ Icc a b
fDiff : DifferentiableOn ℝ f (Ioi 0)
gDiff : DifferentiableOn ℝ g (Ioi 0)
fderivCont : ContinuousOn (deriv f) (Ioi 0)
gderivCont : ContinuousOn (deriv g) (Ioi 0)
Icc_sub : Icc a b ⊆ Ioi 0
fderivSupp : Function.support (deriv f) ⊆ Icc a b
fgSupp : Function.support (f * g) ⊆ Icc a b
fDerivgInt : IntegrableOn (f * deriv g) (Ioi 0) volume
gDerivfInt : IntegrableOn (deriv f * g) (Ioi 0) volume
lim_at_zero : Tendsto (f * g) (𝓝[>] 0) (𝓝 0)
⊢ ∫ (x : ℝ) in Ioi 0, f x * deriv g x = -∫ (x : ℝ) in Ioi 0, deriv f x * g x
Theorem: PartialIntegration_of_support_in_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f g : ℝ → ℂ
ha : 0 < a
h : a ≤ b
fSupp : Function.support f ⊆ Icc a b
fDiff : DifferentiableOn ℝ f (Ioi 0)
gDiff : DifferentiableOn ℝ g (Ioi 0)
fderivCont : ContinuousOn (deriv f) (Ioi 0)
gderivCont : ContinuousOn (deriv g) (Ioi 0)
Icc_sub : Icc a b ⊆ Ioi 0
fderivSupp : Function.support (deriv f) ⊆ Icc a b
fgSupp : Function.support (f * g) ⊆ Icc a b
fDerivgInt : IntegrableOn (f * deriv g) (Ioi 0) volume
gDerivfInt : IntegrableOn (deriv f * g) (Ioi 0) volume
lim_at_zero : Tendsto (f * g) (𝓝[>] 0) (𝓝 0)
⊢ ∫ (x : ℝ) in Ioi 0, f x * deriv g x = -∫ (x : ℝ) in Ioi 0, deriv f x * g x
Tactic:
have lim_at_inf : Tendsto (f * g) atTop (𝓝 0) := TendstoAtTop_of_support_in_Icc (f * g) fgSupp
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f g : ℝ → ℂ
ha : 0 < a
h : a ≤ b
fSupp : Function.support f ⊆ Icc a b
fDiff : DifferentiableOn ℝ f (Ioi 0)
gDiff : DifferentiableOn ℝ g (Ioi 0)
fderivCont : ContinuousOn (deriv f) (Ioi 0)
gderivCont : ContinuousOn (deriv g) (Ioi 0)
Icc_sub : Icc a b ⊆ Ioi 0
fderivSupp : Function.support (deriv f) ⊆ Icc a b
fgSupp : Function.support (f * g) ⊆ Icc a b
fDerivgInt : IntegrableOn (f * deriv g) (Ioi 0) volume
gDerivfInt : IntegrableOn (deriv f * g) (Ioi 0) volume
lim_at_zero : Tendsto (f * g) (𝓝[>] 0) (𝓝 0)
lim_at_inf : Tendsto (f * g) atTop (𝓝 0)
⊢ ∫ (x : ℝ) in Ioi 0, f x * deriv g x = -∫ (x : ℝ) in Ioi 0, deriv f x * g x
Theorem: PartialIntegration_of_support_in_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f g : ℝ → ℂ
ha : 0 < a
h : a ≤ b
fSupp : Function.support f ⊆ Icc a b
fDiff : DifferentiableOn ℝ f (Ioi 0)
gDiff : DifferentiableOn ℝ g (Ioi 0)
fderivCont : ContinuousOn (deriv f) (Ioi 0)
gderivCont : ContinuousOn (deriv g) (Ioi 0)
Icc_sub : Icc a b ⊆ Ioi 0
fderivSupp : Function.support (deriv f) ⊆ Icc a b
fgSupp : Function.support (f * g) ⊆ Icc a b
fDerivgInt : IntegrableOn (f * deriv g) (Ioi 0) volume
gDerivfInt : IntegrableOn (deriv f * g) (Ioi 0) volume
lim_at_zero : Tendsto (f * g) (𝓝[>] 0) (𝓝 0)
lim_at_inf : Tendsto (f * g) atTop (𝓝 0)
⊢ ∫ (x : ℝ) in Ioi 0, f x * deriv g x = -∫ (x : ℝ) in Ioi 0, deriv f x * g x
Tactic:
apply PartialIntegration f g fDiff gDiff fDerivgInt gDerivfInt lim_at_zero lim_at_inf
Proof state after:
no goals
Theorem: PartialIntegration_of_support_in_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f g : ℝ → ℂ
ha : 0 < a
h : a ≤ b
fSupp : Function.support f ⊆ Icc a b
fDiff : DifferentiableOn ℝ f (Ioi 0)
gDiff : DifferentiableOn ℝ g (Ioi 0)
fderivCont : ContinuousOn (deriv f) (Ioi 0)
gderivCont : ContinuousOn (deriv g) (Ioi 0)
Icc_sub : Icc a b ⊆ Ioi 0
fderivSupp : Function.support (deriv f) ⊆ Icc a b
fgSupp : Function.support (f * g) ⊆ Icc a b
⊢ IntegrableOn (f * deriv g) (Ioi 0) volume
Tactic:
apply (integrableOn_iff_integrable_of_support_subset <|
       Function.support_mul_subset_of_subset fSupp).mp
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f g : ℝ → ℂ
ha : 0 < a
h : a ≤ b
fSupp : Function.support f ⊆ Icc a b
fDiff : DifferentiableOn ℝ f (Ioi 0)
gDiff : DifferentiableOn ℝ g (Ioi 0)
fderivCont : ContinuousOn (deriv f) (Ioi 0)
gderivCont : ContinuousOn (deriv g) (Ioi 0)
Icc_sub : Icc a b ⊆ Ioi 0
fderivSupp : Function.support (deriv f) ⊆ Icc a b
fgSupp : Function.support (f * g) ⊆ Icc a b
⊢ IntegrableOn (f * deriv g) (Icc a b) (volume.restrict (Ioi 0))
Theorem: PartialIntegration_of_support_in_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f g : ℝ → ℂ
ha : 0 < a
h : a ≤ b
fSupp : Function.support f ⊆ Icc a b
fDiff : DifferentiableOn ℝ f (Ioi 0)
gDiff : DifferentiableOn ℝ g (Ioi 0)
fderivCont : ContinuousOn (deriv f) (Ioi 0)
gderivCont : ContinuousOn (deriv g) (Ioi 0)
Icc_sub : Icc a b ⊆ Ioi 0
fderivSupp : Function.support (deriv f) ⊆ Icc a b
fgSupp : Function.support (f * g) ⊆ Icc a b
⊢ IntegrableOn (f * deriv g) (Icc a b) (volume.restrict (Ioi 0))
Tactic:
exact fDiff.continuousOn.mono Icc_sub |>.mul (gderivCont.mono Icc_sub) |>.integrableOn_Icc
Proof state after:
no goals
Theorem: PartialIntegration_of_support_in_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f g : ℝ → ℂ
ha : 0 < a
h : a ≤ b
fSupp : Function.support f ⊆ Icc a b
fDiff : DifferentiableOn ℝ f (Ioi 0)
gDiff : DifferentiableOn ℝ g (Ioi 0)
fderivCont : ContinuousOn (deriv f) (Ioi 0)
gderivCont : ContinuousOn (deriv g) (Ioi 0)
Icc_sub : Icc a b ⊆ Ioi 0
fderivSupp : Function.support (deriv f) ⊆ Icc a b
fgSupp : Function.support (f * g) ⊆ Icc a b
fDerivgInt : IntegrableOn (f * deriv g) (Ioi 0) volume
⊢ IntegrableOn (deriv f * g) (Ioi 0) volume
Tactic:
apply (integrableOn_iff_integrable_of_support_subset <|
       Function.support_mul_subset_of_subset fderivSupp).mp
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f g : ℝ → ℂ
ha : 0 < a
h : a ≤ b
fSupp : Function.support f ⊆ Icc a b
fDiff : DifferentiableOn ℝ f (Ioi 0)
gDiff : DifferentiableOn ℝ g (Ioi 0)
fderivCont : ContinuousOn (deriv f) (Ioi 0)
gderivCont : ContinuousOn (deriv g) (Ioi 0)
Icc_sub : Icc a b ⊆ Ioi 0
fderivSupp : Function.support (deriv f) ⊆ Icc a b
fgSupp : Function.support (f * g) ⊆ Icc a b
fDerivgInt : IntegrableOn (f * deriv g) (Ioi 0) volume
⊢ IntegrableOn (deriv f * g) (Icc a b) (volume.restrict (Ioi 0))
Theorem: PartialIntegration_of_support_in_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f g : ℝ → ℂ
ha : 0 < a
h : a ≤ b
fSupp : Function.support f ⊆ Icc a b
fDiff : DifferentiableOn ℝ f (Ioi 0)
gDiff : DifferentiableOn ℝ g (Ioi 0)
fderivCont : ContinuousOn (deriv f) (Ioi 0)
gderivCont : ContinuousOn (deriv g) (Ioi 0)
Icc_sub : Icc a b ⊆ Ioi 0
fderivSupp : Function.support (deriv f) ⊆ Icc a b
fgSupp : Function.support (f * g) ⊆ Icc a b
fDerivgInt : IntegrableOn (f * deriv g) (Ioi 0) volume
⊢ IntegrableOn (deriv f * g) (Icc a b) (volume.restrict (Ioi 0))
Tactic:
exact fderivCont.mono Icc_sub |>.mul (gDiff.continuousOn.mono Icc_sub) |>.integrableOn_Icc
Proof state after:
no goals
Theorem: PerronInverseMellin_lt
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
tpos : 0 < t
t_lt_x : t < x
σ : ℝ
σpos : 0 < σ
⊢ MellinInverseTransform (Perron.f t) σ x = 0
Tactic:
dsimp [MellinInverseTransform, VerticalIntegral']
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
tpos : 0 < t
t_lt_x : t < x
σ : ℝ
σpos : 0 < σ
⊢ 1 / (2 * ↑π * I) * VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 0
Theorem: PerronInverseMellin_lt
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
tpos : 0 < t
t_lt_x : t < x
σ : ℝ
σpos : 0 < σ
⊢ 1 / (2 * ↑π * I) * VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 0
Tactic:
have xpos : 0 < x := lt_trans tpos t_lt_x
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
tpos : 0 < t
t_lt_x : t < x
σ : ℝ
σpos : 0 < σ
xpos : 0 < x
⊢ 1 / (2 * ↑π * I) * VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 0
Theorem: PerronInverseMellin_lt
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
tpos : 0 < t
t_lt_x : t < x
σ : ℝ
σpos : 0 < σ
xpos : 0 < x
⊢ 1 / (2 * ↑π * I) * VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 0
Tactic:
simp only [one_div, mul_inv_rev, inv_I, neg_mul, neg_eq_zero, mul_eq_zero, I_ne_zero,
  inv_eq_zero, ofReal_eq_zero, pi_ne_zero, OfNat.ofNat_ne_zero, or_self, false_or]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
tpos : 0 < t
t_lt_x : t < x
σ : ℝ
σpos : 0 < σ
xpos : 0 < x
⊢ VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 0
Theorem: PerronInverseMellin_lt
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
tpos : 0 < t
t_lt_x : t < x
σ : ℝ
σpos : 0 < σ
xpos : 0 < x
⊢ VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 0
Tactic:
convert Perron.formulaLtOne (div_pos tpos xpos) ((div_lt_one xpos).mpr t_lt_x) σpos using 2
Proof state after:
case h.e'_2.h.e'_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
tpos : 0 < t
t_lt_x : t < x
σ : ℝ
σpos : 0 < σ
xpos : 0 < x
⊢ (fun s => ↑x ^ (-s) * Perron.f t s) = Perron.f (t / x)
Theorem: PerronInverseMellin_lt
Proof state before:
case h.e'_2.h.e'_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
tpos : 0 < t
t_lt_x : t < x
σ : ℝ
σpos : 0 < σ
xpos : 0 < x
⊢ (fun s => ↑x ^ (-s) * Perron.f t s) = Perron.f (t / x)
Tactic:
ext1 s
Proof state after:
case h.e'_2.h.e'_4.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
tpos : 0 < t
t_lt_x : t < x
σ : ℝ
σpos : 0 < σ
xpos : 0 < x
s : ℂ
⊢ ↑x ^ (-s) * Perron.f t s = Perron.f (t / x) s
Theorem: PerronInverseMellin_lt
Proof state before:
case h.e'_2.h.e'_4.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
tpos : 0 < t
t_lt_x : t < x
σ : ℝ
σpos : 0 < σ
xpos : 0 < x
s : ℂ
⊢ ↑x ^ (-s) * Perron.f t s = Perron.f (t / x) s
Tactic:
convert Perron.f_mul_eq_f tpos xpos s using 1
Proof state after:
case h.e'_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
tpos : 0 < t
t_lt_x : t < x
σ : ℝ
σpos : 0 < σ
xpos : 0 < x
s : ℂ
⊢ ↑x ^ (-s) * Perron.f t s = Perron.f t s * ↑x ^ (-s)
Theorem: PerronInverseMellin_lt
Proof state before:
case h.e'_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
tpos : 0 < t
t_lt_x : t < x
σ : ℝ
σpos : 0 < σ
xpos : 0 < x
s : ℂ
⊢ ↑x ^ (-s) * Perron.f t s = Perron.f t s * ↑x ^ (-s)
Tactic:
ring
Proof state after:
no goals
Theorem: PerronInverseMellin_gt
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
⊢ MellinInverseTransform (Perron.f t) σ x = 1 - ↑x / ↑t
Tactic:
dsimp [MellinInverseTransform]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
⊢ 1 / (2 * ↑π * I) * VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 1 - ↑x / ↑t
Theorem: PerronInverseMellin_gt
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
⊢ 1 / (2 * ↑π * I) * VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 1 - ↑x / ↑t
Tactic:
have tpos : 0 < t := by linarith
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
⊢ 1 / (2 * ↑π * I) * VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 1 - ↑x / ↑t
Theorem: PerronInverseMellin_gt
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
⊢ 1 / (2 * ↑π * I) * VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 1 - ↑x / ↑t
Tactic:
have txinv_gtOne : 1 < t / x := (one_lt_div xpos).mpr x_lt_t
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
⊢ 1 / (2 * ↑π * I) * VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 1 - ↑x / ↑t
Theorem: PerronInverseMellin_gt
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
⊢ 1 / (2 * ↑π * I) * VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 1 - ↑x / ↑t
Tactic:
rw [← smul_eq_mul]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
⊢ (1 / (2 * ↑π * I)) • VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 1 - ↑x / ↑t
Theorem: PerronInverseMellin_gt
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
⊢ (1 / (2 * ↑π * I)) • VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 1 - ↑x / ↑t
Tactic:
convert Perron.formulaGtOne txinv_gtOne σpos using 2
Proof state after:
case h.e'_2.h.e'_6
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
⊢ VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = VerticalIntegral (fun s => ↑(t / x) ^ s / (s * (s + 1))) σ

case h.e'_3.h.e'_6
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
⊢ ↑x / ↑t = 1 / ↑(t / x)
Theorem: PerronInverseMellin_gt
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
⊢ 0 < t
Tactic:
linarith
Proof state after:
no goals
Theorem: PerronInverseMellin_gt
Proof state before:
case h.e'_2.h.e'_6
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
⊢ VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = VerticalIntegral (fun s => ↑(t / x) ^ s / (s * (s + 1))) σ
Tactic:
congr
Proof state after:
case h.e'_2.h.e'_6.e_f
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
⊢ (fun s => ↑x ^ (-s) * Perron.f t s) = fun s => ↑(t / x) ^ s / (s * (s + 1))
Theorem: PerronInverseMellin_gt
Proof state before:
case h.e'_2.h.e'_6.e_f
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
⊢ (fun s => ↑x ^ (-s) * Perron.f t s) = fun s => ↑(t / x) ^ s / (s * (s + 1))
Tactic:
ext1 s
Proof state after:
case h.e'_2.h.e'_6.e_f.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
s : ℂ
⊢ ↑x ^ (-s) * Perron.f t s = ↑(t / x) ^ s / (s * (s + 1))
Theorem: PerronInverseMellin_gt
Proof state before:
case h.e'_2.h.e'_6.e_f.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
s : ℂ
⊢ ↑x ^ (-s) * Perron.f t s = ↑(t / x) ^ s / (s * (s + 1))
Tactic:
convert Perron.f_mul_eq_f tpos xpos s using 1
Proof state after:
case h.e'_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
s : ℂ
⊢ ↑x ^ (-s) * Perron.f t s = Perron.f t s * ↑x ^ (-s)
Theorem: PerronInverseMellin_gt
Proof state before:
case h.e'_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
s : ℂ
⊢ ↑x ^ (-s) * Perron.f t s = Perron.f t s * ↑x ^ (-s)
Tactic:
ring
Proof state after:
no goals
Theorem: PerronInverseMellin_gt
Proof state before:
case h.e'_3.h.e'_6
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
⊢ ↑x / ↑t = 1 / ↑(t / x)
Tactic:
field_simp
Proof state after:
no goals