awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
a : E
inst_4 : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
h : α → E := g - t.indicator fun (x : α) ↦ a
⊢ Tendsto (t.indicator fun (x : α) ↦ a) (𝓝[s] x₀) (𝓝 a)
have hcg₁ : EventuallyEq.{u_1, u_2} (β := E) (𝓝[s] x₀) (fun (x : α) ↦ a) (t.indicator fun (x : α) ↦ a)
Tactic: apply tendsto_const_nhds.congr'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
a : E
inst_4 : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
h : α → E := g - t.indicator fun (x : α) ↦ a
⊢ EventuallyEq.{u_1, u_2} (β := E) (𝓝[s] x₀) (fun (x : α) ↦ a) (t.indicator fun (x : α) ↦ a)
have h₁ : ∀ (a_1 : α),
  Membership.mem (γ := Set α)
    {x : α |
      x ∈ t →
        Membership.mem (γ := Set α)
          {x : α | (fun (x : α) ↦ Eq.{u_2 + 1} (α := E) ((fun (x : α) ↦ a) x) (t.indicator (fun (x : α) ↦ a) x)) x} x}
    a_1
Tactic: filter_upwards [h'ts] with x hx using by simp [hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
a : E
inst_4 : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
h : α → E := g - t.indicator fun (x : α) ↦ a
h₁ :
  ∀ (a_1 : α),
    Membership.mem (γ := Set α)
      {x : α |
        x ∈ t →
          Membership.mem (γ := Set α)
            {x : α | (fun (x : α) ↦ Eq.{u_2 + 1} (α := E) ((fun (x : α) ↦ a) x) (t.indicator (fun (x : α) ↦ a) x)) x} x}
      a_1
⊢ EventuallyEq.{u_1, u_2} (β := E) (𝓝[s] x₀) (fun (x : α) ↦ a) (t.indicator fun (x : α) ↦ a)
have h₂ : ∀ a_1 ∈ t, a = t.indicator (fun (x : α) ↦ a) a_1
Tactic: filter_upwards [h'ts] with x hx using by simp [hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (hypothesis)
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
a : E
inst_4 : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
h : α → E := g - t.indicator fun (x : α) ↦ a
⊢ Tendsto (fun (i : ι) ↦ ∫ (x : α) in s, φ i x • g x ∂μ) l (𝓝 a)
have A : Tendsto (fun (i : ι) ↦ ∫ (x : α) in s, φ i x • h x ∂μ + HSMul.hSMul (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) a) l
  (𝓝 (0 + HSMul.hSMul (α := ℝ) 1 a))
Tactic: have A : Tendsto (fun i : ι => (∫ x in s, φ i x • h x ∂μ) + (∫ x in t, φ i x ∂μ) • a) l
      (𝓝 (0 + (1 : ℝ) • a)) := by
    refine Tendsto.add ?_ (Tendsto.smul hiφ tendsto_const_nhds)
    apply tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto_aux hs ht hts h'ts
        hnφ hlφ hiφ h'iφ
    · apply hmg.sub
      simp only [integrableOn_indicator_iff ht, integrableOn_const_iff (C := a)]
      right
      exact lt_of_le_of_lt (measure_mono inter_subset_left) (h't.lt_top)
    · rw [← sub_self a]
      apply Tendsto.sub hcg
      apply tendsto_const_nhds.congr'
      filter_upwards [h'ts] with x hx using by simp [hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (hypothesis)
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
a : E
inst_4 : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
h : α → E := g - t.indicator fun (x : α) ↦ a
A :
  Tendsto (fun (i : ι) ↦ ∫ (x : α) in s, φ i x • h x ∂μ + HSMul.hSMul (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) a) l
    (𝓝 (0 + HSMul.hSMul (α := ℝ) 1 a))
⊢ Tendsto (fun (i : ι) ↦ ∫ (x : α) in s, φ i x • g x ∂μ) l (𝓝 a)
have A₁ : Tendsto (fun (i : ι) ↦ ∫ (x : α) in s, φ i x • h x ∂μ + HSMul.hSMul (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) a) l (𝓝 a)
Tactic: simp only [one_smul, zero_add] at A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
a : E
inst_4 : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
h : α → E := g - t.indicator fun (x : α) ↦ a
A : Tendsto (fun (i : ι) ↦ ∫ (x : α) in s, φ i x • h x ∂μ + HSMul.hSMul (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) a) l (𝓝 a)
⊢ Tendsto (fun (i : ι) ↦ ∫ (x : α) in s, φ i x • g x ∂μ) l (𝓝 a)
have refine : EventuallyEq.{u_3, u_2} (β := E) l
  (fun (i : ι) ↦ ∫ (x : α) in s, φ i x • h x ∂μ + HSMul.hSMul (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) a) fun (i : ι) ↦
  ∫ (x : α) in s, φ i x • g x ∂μ
Tactic: refine Tendsto.congr' ?_ A
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
a : E
inst_4 : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
h : α → E := g - t.indicator fun (x : α) ↦ a
A : Tendsto (fun (i : ι) ↦ ∫ (x : α) in s, φ i x • h x ∂μ + HSMul.hSMul (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) a) l (𝓝 a)
⊢ EventuallyEq.{u_3, u_2} (β := E) l
    (fun (i : ι) ↦ ∫ (x : α) in s, φ i x • h x ∂μ + HSMul.hSMul (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) a) fun (i : ι) ↦
    ∫ (x : α) in s, φ i x • g x ∂μ
have h₁ : ∀ (i : ι) (hi : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ)
  (h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < 1),
  ∫ (x : α) in s, φ i x • h x ∂μ + HSMul.hSMul (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) a = ∫ (x : α) in s, φ i x • g x ∂μ
Tactic: filter_upwards [integrableOn_peak_smul_of_integrableOn_of_tendsto hs h'ts
    hlφ hiφ h'iφ hmg hcg,
    (tendsto_order.1 (tendsto_iff_norm_sub_tendsto_zero.1 hiφ)).2 1 zero_lt_one] with i hi h'i
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
a : E
inst_4 : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
h : α → E := g - t.indicator fun (x : α) ↦ a
A : Tendsto (fun (i : ι) ↦ ∫ (x : α) in s, φ i x • h x ∂μ + HSMul.hSMul (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) a) l (𝓝 a)
i : ι
hi : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < 1
⊢ ∫ (x : α) in s, φ i x • h x ∂μ + HSMul.hSMul (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) a = ∫ (x : α) in s, φ i x • g x ∂μ
have h₁ : ∫ (x : α) in s, φ i x • g x - t.indicator (fun (a_1 : α) ↦ φ i a_1 • a) x ∂μ +
    HSMul.hSMul (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) a =
  ∫ (x : α) in s, φ i x • g x ∂μ
Tactic: simp only [h, Pi.sub_apply, smul_sub, ← indicator_smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
a : E
inst_4 : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
h : α → E := g - t.indicator fun (x : α) ↦ a
A : Tendsto (fun (i : ι) ↦ ∫ (x : α) in s, φ i x • h x ∂μ + HSMul.hSMul (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) a) l (𝓝 a)
i : ι
hi : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < 1
⊢ ∫ (x : α) in s, φ i x • g x - t.indicator (fun (a_1 : α) ↦ φ i a_1 • a) x ∂μ +
      HSMul.hSMul (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) a =
    ∫ (x : α) in s, φ i x • g x ∂μ
have h₁ : Integrable.{u_2, u_1} (ε := E) (t.indicator fun (a_1 : α) ↦ φ i a_1 • a) (μ.restrict s)
Tactic: rw [integral_sub hi, setIntegral_indicator ht, inter_eq_right.mpr hts,
    integral_smul_const, sub_add_cancel]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
a : E
inst_4 : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
h : α → E := g - t.indicator fun (x : α) ↦ a
A : Tendsto (fun (i : ι) ↦ ∫ (x : α) in s, φ i x • h x ∂μ + HSMul.hSMul (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) a) l (𝓝 a)
i : ι
hi : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < 1
⊢ Integrable.{u_2, u_1} (ε := E) (t.indicator fun (a_1 : α) ↦ φ i a_1 • a) (μ.restrict s)
have h₁ : IntegrableOn.{u_1, u_2} (ε := E) (fun (a_1 : α) ↦ φ i a_1 • a) t (μ.restrict s)
Tactic: rw [integrable_indicator_iff ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
a : E
inst_4 : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
h : α → E := g - t.indicator fun (x : α) ↦ a
A : Tendsto (fun (i : ι) ↦ ∫ (x : α) in s, φ i x • h x ∂μ + HSMul.hSMul (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) a) l (𝓝 a)
i : ι
hi : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < 1
⊢ IntegrableOn.{u_1, u_2} (ε := E) (fun (a_1 : α) ↦ φ i a_1 • a) t (μ.restrict s)
have h₁ : Integrable (φ i) ((μ.restrict s).restrict t)
Tactic: apply Integrable.smul_const
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
a : E
inst_4 : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
h : α → E := g - t.indicator fun (x : α) ↦ a
A : Tendsto (fun (i : ι) ↦ ∫ (x : α) in s, φ i x • h x ∂μ + HSMul.hSMul (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) a) l (𝓝 a)
i : ι
hi : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < 1
⊢ Integrable (φ i) ((μ.restrict s).restrict t)
have h₁ : Integrable (φ i) (μ.restrict t)
Tactic: rw [restrict_restrict ht, inter_eq_left.mpr hts]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
φ : ι → α → ℝ
a : E
inst_4 : CompleteSpace E
t : Set α
ht : MeasurableSet t
h'ts : t ∈ 𝓝 x₀
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l uᶜ
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) μ
hmg : Integrable g μ
hcg : Tendsto g (𝓝 x₀) (𝓝 a)
⊢ Tendsto (fun (i : ι) ↦ ∫ (x : α), φ i x • g x ∂μ) l (𝓝 a)
have suffices : Tendsto (fun (i : ι) ↦ ∫ (x : α) in univ, φ i x • g x ∂μ) l (𝓝 a)
Tactic: suffices Tendsto (fun i : ι ↦ ∫ x in univ, φ i x • g x ∂μ) l (𝓝 a) by simpa
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst_4 : CompleteSpace E
inst_5 : MetrizableSpace α
inst_6 : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun (n : ℕ) (x : α) ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
n : ℕ
x : α
hx : x ∈ s
⊢ 0 ≤ φ n x
have apply : LE.le (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
Tactic: apply mul_nonneg (inv_nonneg.2 _) (pow_nonneg (hnc x hx) _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (hypothesis)
Goal:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst_4 : CompleteSpace E
inst_5 : MetrizableSpace α
inst_6 : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun (n : ℕ) (x : α) ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
⊢ Tendsto
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ (∫ (x : α) in s, c x ^ n • g x ∂μ))
    atTop (𝓝 (g x₀))
have hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
Tactic: have hnφ : ∀ n, ∀ x ∈ s, 0 ≤ φ n x := by
    intro n x hx
    apply mul_nonneg (inv_nonneg.2 _) (pow_nonneg (hnc x hx) _)
    exact setIntegral_nonneg hs.measurableSet fun x hx => pow_nonneg (hnc x hx) _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (hypothesis)
Goal:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst_4 : CompleteSpace E
inst_5 : MetrizableSpace α
inst_6 : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun (n : ℕ) (x : α) ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
⊢ Tendsto
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ (∫ (x : α) in s, c x ^ n • g x ∂μ))
    atTop (𝓝 (g x₀))
have I : ∀ (n : ℕ), IntegrableOn (ε := ℝ) (fun (x : α) ↦ c x ^ n) s μ
Tactic: have I : ∀ n, IntegrableOn (fun x => c x ^ n) s μ := fun n =>
    ContinuousOn.integrableOn_compact hs (hc.pow n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst_4 : CompleteSpace E
inst_5 : MetrizableSpace α
inst_6 : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun (n : ℕ) (x : α) ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (ε := ℝ) (fun (x : α) ↦ c x ^ n) s μ
n : ℕ
⊢ (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ c x ^ n
have h : ∀ (x : α) (hx : x ∈ s), 0 x ≤ c x ^ n
Tactic: filter_upwards [ae_restrict_mem hs.measurableSet] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (hypothesis)
Goal:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst_4 : CompleteSpace E
inst_5 : MetrizableSpace α
inst_6 : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun (n : ℕ) (x : α) ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (ε := ℝ) (fun (x : α) ↦ c x ^ n) s μ
⊢ Tendsto
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ (∫ (x : α) in s, c x ^ n • g x ∂μ))
    atTop (𝓝 (g x₀))
have J : ∀ (n : ℕ), (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ c x ^ n
Tactic: have J : ∀ n, 0 ≤ᵐ[μ.restrict s] fun x : α => c x ^ n := by
    intro n
    filter_upwards [ae_restrict_mem hs.measurableSet] with x hx
    exact pow_nonneg (hnc x hx) n
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst_4 : CompleteSpace E
inst_5 : MetrizableSpace α
inst_6 : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun (n : ℕ) (x : α) ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (ε := ℝ) (fun (x : α) ↦ c x ^ n) s μ
J : ∀ (n : ℕ), (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ c x ^ n
n : ℕ
⊢ LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
have refine : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((Function.support (M := ℝ) fun (x : α) ↦ c x ^ n) ∩ s) : ℝ≥0∞)
Tactic: refine (setIntegral_pos_iff_support_of_nonneg_ae (J n) (I n)).2 ?_