Theorem: exists_mul_eq_setInterval_Icc_of_continuousOn (ForML/IntegralMeanValue.lean)

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

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

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

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

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

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

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