Theorem: exists_mul_eq_intervalIntegral (ForML/IntegralMeanValue.lean)

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]
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 ∂μ

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]
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 ∂μ

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

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

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

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

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

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

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.Ioc a b)
Tactic:
exact h_int.left
State after:
no goals