internlm/Lean-Github huggingface dataset:
Theorem: exists_mul_eq_setInterval
Proof state before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_4
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_ne : Set.Nonempty s
hs_meas : MeasurableSet s
hs_conn : IsPreconnected s
hs_closed : IsClosed s
hf_cont : ContinuousOn f s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
h_int : IntegrableOn (fun x => f x * g x) s
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ nhdsWithin M s ≤ Filter.principal s
Tactic:
simp
Proof state after:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_4
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_ne : Set.Nonempty s
hs_meas : MeasurableSet s
hs_conn : IsPreconnected s
hs_closed : IsClosed s
hf_cont : ContinuousOn f s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
h_int : IntegrableOn (fun x => f x * g x) s
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ s ∈ nhdsWithin M s
Theorem: exists_mul_eq_setInterval
Proof state before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_4
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_ne : Set.Nonempty s
hs_meas : MeasurableSet s
hs_conn : IsPreconnected s
hs_closed : IsClosed s
hf_cont : ContinuousOn f s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
h_int : IntegrableOn (fun x => f x * g x) s
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ s ∈ nhdsWithin M s
Tactic:
exact self_mem_nhdsWithin
Proof state after:
no goals
Theorem: exists_mul_eq_setInterval
Proof state before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_5
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_ne : Set.Nonempty s
hs_meas : MeasurableSet s
hs_conn : IsPreconnected s
hs_closed : IsClosed s
hf_cont : ContinuousOn f s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
h_int : IntegrableOn (fun x => f x * g x) s
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ Filter.Tendsto f (nhdsWithin m s) (nhds (f m))
Tactic:
exact hf_cont m hm_mem
Proof state after:
no goals
Theorem: exists_mul_eq_setInterval
Proof state before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_6
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_ne : Set.Nonempty s
hs_meas : MeasurableSet s
hs_conn : IsPreconnected s
hs_closed : IsClosed s
hf_cont : ContinuousOn f s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
h_int : IntegrableOn (fun x => f x * g x) s
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ Filter.Tendsto f (nhdsWithin M s) (nhds (f M))
Tactic:
exact hf_cont M hM_mem
Proof state after:
no goals
Theorem: Filter_eventuallyLe_restrict_of_forall_mem_imp
Proof state before:
α : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : LE E
f g : α → E
s : Set α
hs : MeasurableSet s
μ : Measure α
h : ∀ x ∈ s, f x ≤ g x
⊢ f ≤ᵐ[Measure.restrict μ s] g
Tactic:
rw [Filter.EventuallyLE]
Proof state after:
α : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : LE E
f g : α → E
s : Set α
hs : MeasurableSet s
μ : Measure α
h : ∀ x ∈ s, f x ≤ g x
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, f x ≤ g x
Theorem: Filter_eventuallyLe_restrict_of_forall_mem_imp
Proof state before:
α : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : LE E
f g : α → E
s : Set α
hs : MeasurableSet s
μ : Measure α
h : ∀ x ∈ s, f x ≤ g x
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, f x ≤ g x
Tactic:
rw [ae_restrict_iff' hs]
Proof state after:
α : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : LE E
f g : α → E
s : Set α
hs : MeasurableSet s
μ : Measure α
h : ∀ x ∈ s, f x ≤ g x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
Theorem: Filter_eventuallyLe_restrict_of_forall_mem_imp
Proof state before:
α : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : LE E
f g : α → E
s : Set α
hs : MeasurableSet s
μ : Measure α
h : ∀ x ∈ s, f x ≤ g x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
Tactic:
exact Filter.eventually_of_forall h
Proof state after:
no goals
Theorem: exists_mul_eq_setInterval_Ici
Proof state before:
a : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Ici a)
hg_int : IntegrableOn g (Set.Ici a)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Ici a)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Ici a)
⊢ ∃ c ∈ Set.Ici a, ∫ (x : ℝ) in Set.Ici a, f x * g x ∂μ = f c * ∫ (x : ℝ) in Set.Ici a, g x ∂μ
Tactic:
apply exists_mul_eq_setInterval hf_cont hg_int hg_nonneg h_int <;> try simp
Proof state after:
a : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Ici a)
hg_int : IntegrableOn g (Set.Ici a)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Ici a)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Ici a)
⊢ IsPreconnected (Set.Ici a)

a : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Ici a)
hg_int : IntegrableOn g (Set.Ici a)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Ici a)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Ici a)
⊢ IsClosed (Set.Ici a)
Theorem: exists_mul_eq_setInterval_Ici
Proof state before:
a : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Ici a)
hg_int : IntegrableOn g (Set.Ici a)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Ici a)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Ici a)
⊢ IsPreconnected (Set.Ici a)

a : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Ici a)
hg_int : IntegrableOn g (Set.Ici a)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Ici a)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Ici a)
⊢ IsClosed (Set.Ici a)
Tactic:
repeat simp [isClosed_Ici, isPreconnected_Ici]
Proof state after:
no goals
Theorem: exists_mul_eq_setInterval_Ici
Proof state before:
a : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Ici a)
hg_int : IntegrableOn g (Set.Ici a)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Ici a)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Ici a)
⊢ MeasurableSet (Set.Ici a)
Tactic:
simp
Proof state after:
no goals
Theorem: exists_mul_eq_setInterval_Ici
Proof state before:
a : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Ici a)
hg_int : IntegrableOn g (Set.Ici a)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Ici a)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Ici a)
⊢ IsClosed (Set.Ici a)
Tactic:
simp [isClosed_Ici, isPreconnected_Ici]
Proof state after:
no goals
Theorem: exists_mul_eq_setInterval_Iic
Proof state before:
a : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Iic a)
hg_int : IntegrableOn g (Set.Iic a)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Iic a)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Iic a)
⊢ ∃ c ∈ Set.Iic a, ∫ (x : ℝ) in Set.Iic a, f x * g x ∂μ = f c * ∫ (x : ℝ) in Set.Iic a, g x ∂μ
Tactic:
apply exists_mul_eq_setInterval hf_cont hg_int hg_nonneg h_int <;> try simp
Proof state after:
a : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Iic a)
hg_int : IntegrableOn g (Set.Iic a)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Iic a)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Iic a)
⊢ IsPreconnected (Set.Iic a)

a : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Iic a)
hg_int : IntegrableOn g (Set.Iic a)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Iic a)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Iic a)
⊢ IsClosed (Set.Iic a)
Theorem: exists_mul_eq_setInterval_Iic
Proof state before:
a : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Iic a)
hg_int : IntegrableOn g (Set.Iic a)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Iic a)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Iic a)
⊢ IsPreconnected (Set.Iic a)

a : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Iic a)
hg_int : IntegrableOn g (Set.Iic a)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Iic a)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Iic a)
⊢ IsClosed (Set.Iic a)
Tactic:
repeat simp [isClosed_Iic, isPreconnected_Iic]
Proof state after:
no goals
Theorem: exists_mul_eq_setInterval_Iic
Proof state before:
a : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Iic a)
hg_int : IntegrableOn g (Set.Iic a)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Iic a)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Iic a)
⊢ MeasurableSet (Set.Iic a)
Tactic:
simp
Proof state after:
no goals
Theorem: exists_mul_eq_setInterval_Iic
Proof state before:
a : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Iic a)
hg_int : IntegrableOn g (Set.Iic a)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Iic a)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Iic a)
⊢ IsClosed (Set.Iic a)
Tactic:
simp [isClosed_Iic, isPreconnected_Iic]
Proof state after:
no goals
Theorem: exists_mul_eq_setInterval_Icc
Proof state before:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntegrableOn g (Set.Icc a b)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Icc a b)
⊢ ∃ c ∈ Set.Icc a b, ∫ (x : ℝ) in Set.Icc a b, f x * g x ∂μ = f c * ∫ (x : ℝ) in Set.Icc a b, g x ∂μ
Tactic:
apply exists_mul_eq_setInterval hf_cont hg_int hg_nonneg h_int <;> try simp [hab]
Proof state after:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntegrableOn g (Set.Icc a b)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Icc a b)
⊢ IsPreconnected (Set.Icc a b)

a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntegrableOn g (Set.Icc a b)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Icc a b)
⊢ IsClosed (Set.Icc a b)
Theorem: exists_mul_eq_setInterval_Icc
Proof state before:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntegrableOn g (Set.Icc a b)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Icc a b)
⊢ IsPreconnected (Set.Icc a b)

a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntegrableOn g (Set.Icc a b)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Icc a b)
⊢ IsClosed (Set.Icc a b)
Tactic:
repeat simp [isClosed_Icc, isPreconnected_Icc, hab]
Proof state after:
no goals
Theorem: exists_mul_eq_setInterval_Icc
Proof state before:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntegrableOn g (Set.Icc a b)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Icc a b)
⊢ MeasurableSet (Set.Icc a b)
Tactic:
simp [hab]
Proof state after:
no goals
Theorem: exists_mul_eq_setInterval_Icc
Proof state before:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntegrableOn g (Set.Icc a b)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Icc a b)
⊢ IsClosed (Set.Icc a b)
Tactic:
simp [isClosed_Icc, isPreconnected_Icc, hab]
Proof state after:
no goals
Theorem: exists_mul_eq_setInterval_Icc_of_continuousOn
Proof state before:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_cont : ContinuousOn g (Set.Icc a b)
hg_nonneg : ∀ x ∈ Set.Icc a b, 0 ≤ g x
⊢ ∃ c ∈ Set.Icc a b, ∫ (x : ℝ) in Set.Icc a b, f x * g x ∂μ = f c * ∫ (x : ℝ) in Set.Icc a b, g x ∂μ
Tactic:
apply exists_mul_eq_setInterval_Icc hab hf_cont ?_ ?_ ?_
Proof state after:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_cont : ContinuousOn g (Set.Icc a b)
hg_nonneg : ∀ x ∈ Set.Icc a b, 0 ≤ g x
⊢ IntegrableOn (fun x => g x) (Set.Icc a b)

a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_cont : ContinuousOn g (Set.Icc a b)
hg_nonneg : ∀ x ∈ Set.Icc a b, 0 ≤ g x
⊢ 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] fun x => g x

a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_cont : ContinuousOn g (Set.Icc a b)
hg_nonneg : ∀ x ∈ Set.Icc a b, 0 ≤ g x
⊢ IntegrableOn (fun x => f x * g x) (Set.Icc a b)
Theorem: exists_mul_eq_setInterval_Icc_of_continuousOn
Proof state before:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_cont : ContinuousOn g (Set.Icc a b)
hg_nonneg : ∀ x ∈ Set.Icc a b, 0 ≤ g x
⊢ IntegrableOn (fun x => g x) (Set.Icc a b)

a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_cont : ContinuousOn g (Set.Icc a b)
hg_nonneg : ∀ x ∈ Set.Icc a b, 0 ≤ g x
⊢ 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] fun x => g x

a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_cont : ContinuousOn g (Set.Icc a b)
hg_nonneg : ∀ x ∈ Set.Icc a b, 0 ≤ g x
⊢ IntegrableOn (fun x => f x * g x) (Set.Icc a b)
Tactic:
. exact ContinuousOn.integrableOn_Icc hg_cont
Proof state after:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_cont : ContinuousOn g (Set.Icc a b)
hg_nonneg : ∀ x ∈ Set.Icc a b, 0 ≤ g x
⊢ 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] fun x => g x

a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_cont : ContinuousOn g (Set.Icc a b)
hg_nonneg : ∀ x ∈ Set.Icc a b, 0 ≤ g x
⊢ IntegrableOn (fun x => f x * g x) (Set.Icc a b)
Theorem: exists_mul_eq_setInterval_Icc_of_continuousOn
Proof state before:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_cont : ContinuousOn g (Set.Icc a b)
hg_nonneg : ∀ x ∈ Set.Icc a b, 0 ≤ g x
⊢ 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] fun x => g x

a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_cont : ContinuousOn g (Set.Icc a b)
hg_nonneg : ∀ x ∈ Set.Icc a b, 0 ≤ g x
⊢ IntegrableOn (fun x => f x * g x) (Set.Icc a b)
Tactic:
. exact Filter_eventuallyLe_restrict_of_forall_mem_imp measurableSet_Icc hg_nonneg
Proof state after:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_cont : ContinuousOn g (Set.Icc a b)
hg_nonneg : ∀ x ∈ Set.Icc a b, 0 ≤ g x
⊢ IntegrableOn (fun x => f x * g x) (Set.Icc a b)
Theorem: exists_mul_eq_setInterval_Icc_of_continuousOn
Proof state before:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_cont : ContinuousOn g (Set.Icc a b)
hg_nonneg : ∀ x ∈ Set.Icc a b, 0 ≤ g x
⊢ IntegrableOn (fun x => f x * g x) (Set.Icc a b)
Tactic:
. exact ContinuousOn.integrableOn_Icc (ContinuousOn.mul hf_cont hg_cont)
Proof state after:
no goals
Theorem: exists_mul_eq_setInterval_Icc_of_continuousOn
Proof state before:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_cont : ContinuousOn g (Set.Icc a b)
hg_nonneg : ∀ x ∈ Set.Icc a b, 0 ≤ g x
⊢ IntegrableOn (fun x => g x) (Set.Icc a b)
Tactic:
exact ContinuousOn.integrableOn_Icc hg_cont
Proof state after:
no goals
Theorem: exists_mul_eq_setInterval_Icc_of_continuousOn
Proof state before:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_cont : ContinuousOn g (Set.Icc a b)
hg_nonneg : ∀ x ∈ Set.Icc a b, 0 ≤ g x
⊢ 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] fun x => g x
Tactic:
exact Filter_eventuallyLe_restrict_of_forall_mem_imp measurableSet_Icc hg_nonneg
Proof state after:
no goals
Theorem: exists_mul_eq_setInterval_Icc_of_continuousOn
Proof state before:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_cont : ContinuousOn g (Set.Icc a b)
hg_nonneg : ∀ x ∈ Set.Icc a b, 0 ≤ g x
⊢ IntegrableOn (fun x => f x * g x) (Set.Icc a b)
Tactic:
exact ContinuousOn.integrableOn_Icc (ContinuousOn.mul hf_cont hg_cont)
Proof state after:
no goals
Theorem: exists_mul_eq_intervalIntegral
Proof state before:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝¹ : NoAtoms μ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntervalIntegrable g μ a b
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntervalIntegrable (fun x => f x * g x) μ a b
⊢ ∃ c ∈ Set.Icc a b, ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
Tactic:
simp only [intervalIntegral.integral_of_le hab]
Proof state after:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝¹ : NoAtoms μ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntervalIntegrable g μ a b
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntervalIntegrable (fun x => f x * g x) μ a b
⊢ ∃ c ∈ Set.Icc a b, ∫ (x : ℝ) in Set.Ioc a b, f x * g x ∂μ = f c * ∫ (x : ℝ) in Set.Ioc a b, g x ∂μ
Theorem: exists_mul_eq_intervalIntegral
Proof state before:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝¹ : NoAtoms μ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntervalIntegrable g μ a b
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntervalIntegrable (fun x => f x * g x) μ a b
⊢ ∃ c ∈ Set.Icc a b, ∫ (x : ℝ) in Set.Ioc a b, f x * g x ∂μ = f c * ∫ (x : ℝ) in Set.Ioc a b, g x ∂μ
Tactic:
simp only [← integral_Icc_eq_integral_Ioc]
Proof state after:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝¹ : NoAtoms μ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntervalIntegrable g μ a b
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntervalIntegrable (fun x => f x * g x) μ a b
⊢ ∃ c ∈ Set.Icc a b, ∫ (x : ℝ) in Set.Icc a b, f x * g x ∂μ = f c * ∫ (x : ℝ) in Set.Icc a b, g x ∂μ
Theorem: exists_mul_eq_intervalIntegral
Proof state before:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝¹ : NoAtoms μ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntervalIntegrable g μ a b
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntervalIntegrable (fun x => f x * g x) μ a b
⊢ ∃ c ∈ Set.Icc a b, ∫ (x : ℝ) in Set.Icc a b, f x * g x ∂μ = f c * ∫ (x : ℝ) in Set.Icc a b, g x ∂μ
Tactic:
refine exists_mul_eq_setInterval_Icc hab hf_cont ?_ hg_nonneg ?_
Proof state after:
case refine_1
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝¹ : NoAtoms μ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntervalIntegrable g μ a b
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntervalIntegrable (fun x => f x * g x) μ a b
⊢ IntegrableOn (fun x => g x) (Set.Icc a b)

case refine_2
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝¹ : NoAtoms μ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntervalIntegrable g μ a b
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntervalIntegrable (fun x => f x * g x) μ a b
⊢ IntegrableOn (fun x => f x * g x) (Set.Icc a b)
Theorem: exists_mul_eq_intervalIntegral
Proof state before:
case refine_1
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝¹ : NoAtoms μ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntervalIntegrable g μ a b
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntervalIntegrable (fun x => f x * g x) μ a b
⊢ IntegrableOn (fun x => g x) (Set.Icc a b)

case refine_2
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝¹ : NoAtoms μ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntervalIntegrable g μ a b
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntervalIntegrable (fun x => f x * g x) μ a b
⊢ IntegrableOn (fun x => f x * g x) (Set.Icc a b)
Tactic:
. rw [integrableOn_Icc_iff_integrableOn_Ioc]
  exact hg_int.left
Proof state after:
case refine_2
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝¹ : NoAtoms μ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntervalIntegrable g μ a b
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntervalIntegrable (fun x => f x * g x) μ a b
⊢ IntegrableOn (fun x => f x * g x) (Set.Icc a b)
Theorem: exists_mul_eq_intervalIntegral
Proof state before:
case refine_2
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝¹ : NoAtoms μ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntervalIntegrable g μ a b
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntervalIntegrable (fun x => f x * g x) μ a b
⊢ IntegrableOn (fun x => f x * g x) (Set.Icc a b)
Tactic:
. rw [integrableOn_Icc_iff_integrableOn_Ioc]
  exact h_int.left
Proof state after:
no goals
Theorem: exists_mul_eq_intervalIntegral
Proof state before:
case refine_1
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝¹ : NoAtoms μ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntervalIntegrable g μ a b
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntervalIntegrable (fun x => f x * g x) μ a b
⊢ IntegrableOn (fun x => g x) (Set.Icc a b)
Tactic:
rw [integrableOn_Icc_iff_integrableOn_Ioc]
Proof state after:
case refine_1
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝¹ : NoAtoms μ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntervalIntegrable g μ a b
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntervalIntegrable (fun x => f x * g x) μ a b
⊢ IntegrableOn (fun x => g x) (Set.Ioc a b)
Theorem: exists_mul_eq_intervalIntegral
Proof state before:
case refine_1
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝¹ : NoAtoms μ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntervalIntegrable g μ a b
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntervalIntegrable (fun x => f x * g x) μ a b
⊢ IntegrableOn (fun x => g x) (Set.Ioc a b)
Tactic:
exact hg_int.left
Proof state after:
no goals
Theorem: exists_mul_eq_intervalIntegral
Proof state before:
case refine_2
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝¹ : NoAtoms μ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntervalIntegrable g μ a b
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntervalIntegrable (fun x => f x * g x) μ a b
⊢ IntegrableOn (fun x => f x * g x) (Set.Icc a b)
Tactic:
rw [integrableOn_Icc_iff_integrableOn_Ioc]
Proof state after:
case refine_2
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝¹ : NoAtoms μ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntervalIntegrable g μ a b
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntervalIntegrable (fun x => f x * g x) μ a b
⊢ IntegrableOn (fun x => f x * g x) (Set.Ioc a b)