awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
i : ι
hif : IntegrableOn f (a i) μ
hig : Integrable (g i) μ
hisupp : support (g i) ⊆ a i
hibound : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
⊢ Integrable.{u_2, u_1} (ε := E) (fun (y : α) ↦ g i y • (f y - c)) μ
have h : Integrable.{u_2, u_1} (ε := E) (fun (y : α) ↦ g i y • f y - g i y • c) μ
Tactic: simp_rw [smul_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
i : ι
hif : IntegrableOn f (a i) μ
hig : Integrable (g i) μ
hisupp : support (g i) ⊆ a i
hibound : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
⊢ Integrable.{u_2, u_1} (ε := E) (fun (y : α) ↦ g i y • f y - g i y • c) μ
have apply : Integrable.{u_2, u_1} (ε := E) (fun (y : α) ↦ g i y • f y) μ
Tactic: apply Integrable.sub _ (hig.smul_const _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
i : ι
hif : IntegrableOn f (a i) μ
hig : Integrable (g i) μ
hisupp : support (g i) ⊆ a i
hibound : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
⊢ (support.{u_1, u_2} (M := E) fun (y : α) ↦ g i y • f y) ⊆ a i
have apply : (support.{u_1, u_2} (M := E) fun (y : α) ↦ g i y • f y) ⊆ support (g i)
Tactic: apply Subset.trans _ hisupp
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
i : ι
hif : IntegrableOn f (a i) μ
hig : Integrable (g i) μ
hisupp : support (g i) ⊆ a i
hibound : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
⊢ Integrable.{u_2, u_1} (ε := E) (fun (y : α) ↦ g i y • f y) μ
have A : (support.{u_1, u_2} (M := E) fun (y : α) ↦ g i y • f y) ⊆ a i
Tactic: have A : Function.support (fun y ↦ g i y • f y) ⊆ a i := by
        apply Subset.trans _ hisupp
        exact Function.support_smul_subset_left _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
i : ι
hif : IntegrableOn f (a i) μ
hig : Integrable (g i) μ
hisupp : support (g i) ⊆ a i
hibound : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
A : (support.{u_1, u_2} (M := E) fun (y : α) ↦ g i y • f y) ⊆ a i
⊢ Integrable.{u_2, u_1} (ε := E) (fun (y : α) ↦ g i y • f y) μ
have rw : IntegrableOn.{u_1, u_2} (ε := E) (fun (y : α) ↦ g i y • f y) (a i) μ
Tactic: rw [← integrableOn_iff_integrable_of_support_subset A]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
i : ι
hif : IntegrableOn f (a i) μ
hig : Integrable (g i) μ
hisupp : support (g i) ⊆ a i
hibound : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
A : (support.{u_1, u_2} (M := E) fun (y : α) ↦ g i y • f y) ⊆ a i
⊢ IntegrableOn.{u_1, u_2} (ε := E) (fun (y : α) ↦ g i y • f y) (a i) μ
have apply : MemLp (g i) ∞ (μ.restrict (a i))
Tactic: apply Integrable.smul_of_top_right hif
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
⊢ Tendsto (fun (i : ι) ↦ ∫ (y : α), g i y • f y ∂μ) l (𝓝 c)
have I : ∀ᶠ (i : ι) in l,
  ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
Tactic: have I : ∀ᶠ i in l, ∫ y, g i y • (f y - c) ∂μ + (∫ y, g i y ∂μ) • c = ∫ y, g i y • f y ∂μ := by
    filter_upwards [f_int, g_int, g_supp, g_bound] with i hif hig hisupp hibound
    rw [← integral_smul_const, ← integral_add]
    · simp only [smul_sub, sub_add_cancel]
    · simp_rw [smul_sub]
      apply Integrable.sub _ (hig.smul_const _)
      have A : Function.support (fun y ↦ g i y • f y) ⊆ a i := by
        apply Subset.trans _ hisupp
        exact Function.support_smul_subset_left _ _
      rw [← integrableOn_iff_integrable_of_support_subset A]
      apply Integrable.smul_of_top_right hif
      exact memLp_top_of_bound hig.aestronglyMeasurable.restrict
        (K / μ.real (a i)) (Eventually.of_forall hibound)
    · exact hig.smul_const _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
⊢ Tendsto.{u_4, u_2} (β := E) (fun (i : ι) ↦ ∫ (y : α), g i y • (f y - c) ∂μ) l (𝓝 0)
have this : Tendsto (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 (K * 0))
Tactic: have := hf.const_mul K
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 (K * 0))
⊢ Tendsto.{u_4, u_2} (β := E) (fun (i : ι) ↦ ∫ (y : α), g i y • (f y - c) ∂μ) l (𝓝 0)
have this₁ : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
Tactic: simp only [mul_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
⊢ Tendsto.{u_4, u_2} (β := E) (fun (i : ι) ↦ ∫ (y : α), g i y • (f y - c) ∂μ) l (𝓝 0)
have refine : ∀ᶠ (n : ι) in l, norm.{u_2} (E := E) (∫ (y : α), g n y • (f y - c) ∂μ) ≤ K * ⨍ (y : α) in a n, ‖f y - c‖ ∂μ
Tactic: refine squeeze_zero_norm' ?_ this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
⊢ ∀ᶠ (n : ι) in l, norm.{u_2} (E := E) (∫ (y : α), g n y • (f y - c) ∂μ) ≤ K * ⨍ (y : α) in a n, ‖f y - c‖ ∂μ
have h : ∀ (i : ι) (hi : support (g i) ⊆ a i) (h'i : ∀ (x : α), |g i x| ≤ K / μ.real (a i)) (h''i : IntegrableOn f (a i) μ)
  (hi_int : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)),
  norm.{u_2} (E := E) (∫ (y : α), g i y • (f y - c) ∂μ) ≤ K * ⨍ (y : α) in a i, ‖f y - c‖ ∂μ
Tactic: filter_upwards [g_supp, g_bound, f_int, (tendsto_order.1 hg).1 _ zero_lt_one]
      with i hi h'i h''i hi_int
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h'i : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
h''i : IntegrableOn f (a i) μ
hi_int : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (a i) : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (a i) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [lt_top_iff_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h'i : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
h''i : IntegrableOn f (a i) μ
hi_int : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (a i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ False
have h'i₁ : ∀ (x : α), g i x = 0
Tactic: simp only [h, ENNReal.toReal_top, _root_.div_zero, abs_nonpos_iff, measureReal_def] at h'i
Cleared hypotheses: h'i
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h''i : IntegrableOn f (a i) μ
hi_int : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (a i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h'i : ∀ (x : α), g i x = 0
⊢ Eq (α := ℝ) (∫ (y : α), g i y ∂μ) (∫ (y : α), 0 ∂μ)
have e_f : Eq.{u_1 + 1} (α := α → ℝ) (fun (y : α) ↦ g i y) fun (y : α) ↦ 0
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h''i : IntegrableOn f (a i) μ
hi_int : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (a i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h'i : ∀ (x : α), g i x = 0
⊢ False
have this₁ : Eq (α := ℝ) (∫ (y : α), g i y ∂μ) (∫ (y : α), 0 ∂μ)
Tactic: have : ∫ (y : α), g i y ∂μ = ∫ (y : α), 0 ∂μ := by congr; ext y; exact h'i y
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h'i : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
h''i : IntegrableOn f (a i) μ
hi_int : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)
⊢ norm.{u_2} (E := E) (∫ (y : α), g i y • (f y - c) ∂μ) ≤ K * ⨍ (y : α) in a i, ‖f y - c‖ ∂μ
have mu_ai : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (a i) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have mu_ai : μ (a i) < ∞ := by
      rw [lt_top_iff_ne_top]
      intro h
      simp only [h, ENNReal.toReal_top, _root_.div_zero, abs_nonpos_iff, measureReal_def] at h'i
      have : ∫ (y : α), g i y ∂μ = ∫ (y : α), 0 ∂μ := by congr; ext y; exact h'i y
      simp [this] at hi_int
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h'i : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
h''i : IntegrableOn f (a i) μ
hi_int : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)
mu_ai : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (a i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ norm.{u_2} (E := E) (∫ (y : α), g i y • (f y - c) ∂μ) ≤ K * ⨍ (y : α) in a i, ‖f y - c‖ ∂μ
have h : ∫ (a : α), ‖g i a • (f a - c)‖ ∂μ ≤ K * ⨍ (y : α) in a i, ‖f y - c‖ ∂μ
Tactic: apply (norm_integral_le_integral_norm _).trans
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h'i : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
h''i : IntegrableOn f (a i) μ
hi_int : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)
mu_ai : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (a i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫ (a : α), ‖g i a • (f a - c)‖ ∂μ ≤ K * ⨍ (y : α) in a i, ‖f y - c‖ ∂μ
have h : LE.le (α := ℝ) (∫ (a : α), ‖g i a‖ * ‖f a - c‖ ∂μ)
  (∫ (a_1 : α) in a i, K / (μ.restrict (a i)).real univ * ‖f a_1 - c‖ ∂μ)
Tactic: simp_rw [average_eq, smul_eq_mul, ← integral_const_mul, norm_smul, ← mul_assoc,
      ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h'i : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
h''i : IntegrableOn f (a i) μ
hi_int : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)
mu_ai : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (a i) : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : x ∉ a i
⊢ g i x = 0
have rw : x ∉ support (g i)
Tactic: rw [← Function.notMem_support]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h'i : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
h''i : IntegrableOn f (a i) μ
hi_int : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)
mu_ai : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (a i) : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : x ∉ a i
⊢ ‖g i x‖ * ‖f x - c‖ = 0
have this₁ : g i x = 0
Tactic: have : g i x = 0 := by rw [← Function.notMem_support]; exact fun h ↦ hx (hi h)