Theorem: PartialIntegration_of_support_in_Icc (PrimeNumberTheoremAnd/MellinCalculus.lean)

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
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))

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
State after:
no goals

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
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))

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
State after:
no goals