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 t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
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₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
hfi : IntegrableOn (ε := ℝ) (fun (x : α) ↦ ‖φ i x‖ * δ) t μ
⊢ LE.le (α := ℝ) (∫ (x : α) in s ∩ u, ‖φ i x‖ * δ ∂μ) (∫ (x : α) in t, ‖φ i x‖ * δ ∂μ)
have hf : (ae (μ.restrict t)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ ‖φ i x‖ * δ
Tactic: apply setIntegral_mono_set
-- 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 t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
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₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
hfi : IntegrableOn (ε := ℝ) (fun (x : α) ↦ ‖φ i x‖ * δ) t μ
hf : (ae (μ.restrict t)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ ‖φ i x‖ * δ
⊢ LE.le (α := ℝ) (∫ (x : α) in s ∩ u, ‖φ i x‖ * δ ∂μ) (∫ (x : α) in t, ‖φ i x‖ * δ ∂μ)
have hst : s ∩ u ≤ᶠ[ae μ] t
Tactic: apply setIntegral_mono_set
-- 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 t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
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₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
⊢ Eq (α := ℝ) (∫ (x : α) in t, ‖φ i x‖ * δ ∂μ) (∫ (x : α) in t, φ i x * δ ∂μ)
have apply : ∀ (x : α) (hx : x ∈ t), ‖φ i x‖ * δ = φ i x * δ
Tactic: apply setIntegral_congr_fun ht fun x 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 t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
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₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
x : α
hx : x ∈ t
⊢ ‖φ i x‖ * δ = φ i x * δ
have rw : φ i x * δ = φ i x * δ
Tactic: rw [Real.norm_of_nonneg (hφpos _ (hts 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 t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
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₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
⊢ ∫ (x : α) in t, φ i x * δ ∂μ = (∫ (x : α) in t, φ i x ∂μ) * δ
have rw : (∫ (a : α) in t, φ i a ∂μ) * δ = (∫ (x : α) in t, φ i x ∂μ) * δ
Tactic: rw [integral_mul_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 t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
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₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
⊢ (∫ (x : α) in t, φ i x ∂μ) * δ ≤ 2 * δ
have hbc : LE.le (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 2
Tactic: gcongr
-- 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 t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
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₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
⊢ LE.le (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 2
have linarith : LT.lt (α := ℝ) 2 (∫ (x : α) in t, φ i x ∂μ) →
  δ - 1 + HSub.hSub (α := ℝ) 2 (∫ (x : α) in t, φ i x ∂μ) + (HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1 - δ) = 0
Tactic: linarith [(le_abs_self _).trans h'i.le]
-- 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 t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
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₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
⊢ norm.{u_2} (E := E) (∫ (x : α) in s, φ i x • g x ∂μ) ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ
have B : norm.{u_2} (E := E) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ) ≤ 2 * δ
Tactic: have B : ‖∫ x in s ∩ u, φ i x • g x ∂μ‖ ≤ 2 * δ :=
    calc
      ‖∫ x in s ∩ u, φ i x • g x ∂μ‖ ≤ ∫ x in s ∩ u, ‖φ i x • g x‖ ∂μ :=
        norm_integral_le_integral_norm _
      _ ≤ ∫ x in s ∩ u, ‖φ i x‖ * δ ∂μ := by
        refine setIntegral_mono_on ?_ ?_ (hs.inter u_open.measurableSet) fun x hx => ?_
        · exact IntegrableOn.mono_set h''i.norm inter_subset_left
        · exact IntegrableOn.mono_set (I.norm.mul_const _) ut
        rw [norm_smul]
        gcongr
        rw [inter_comm] at hu
        exact (mem_ball_zero_iff.1 (hu x hx)).le
      _ ≤ ∫ x in t, ‖φ i x‖ * δ ∂μ := by
        apply setIntegral_mono_set
        · exact I.norm.mul_const _
        · exact Eventually.of_forall fun x => mul_nonneg (norm_nonneg _) δpos.le
        · exact Eventually.of_forall ut
      _ = ∫ x in t, φ i x * δ ∂μ := by
        apply setIntegral_congr_fun ht fun x hx => ?_
        rw [Real.norm_of_nonneg (hφpos _ (hts hx))]
      _ = (∫ x in t, φ i x ∂μ) * δ := by rw [integral_mul_const]
      _ ≤ 2 * δ := by gcongr; linarith [(le_abs_self _).trans h'i.le]
-- 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 t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
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₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : norm.{u_2} (E := E) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ) ≤ 2 * δ
⊢ LE.le (α := ℝ) (∫ (x : α) in s \ u, ‖φ i x • g x‖ ∂μ) (∫ (x : α) in s \ u, δ * ‖g x‖ ∂μ)
have refine_1 : IntegrableOn (ε := ℝ) (fun (x : α) ↦ ‖φ i x • g x‖) (s \ u) μ
Tactic: refine setIntegral_mono_on ?_ ?_ (hs.diff u_open.measurableSet) fun x 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 t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
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₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : norm.{u_2} (E := E) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ) ≤ 2 * δ
refine_1 : IntegrableOn (ε := ℝ) (fun (x : α) ↦ ‖φ i x • g x‖) (s \ u) μ
⊢ LE.le (α := ℝ) (∫ (x : α) in s \ u, ‖φ i x • g x‖ ∂μ) (∫ (x : α) in s \ u, δ * ‖g x‖ ∂μ)
have refine_2 : IntegrableOn (ε := ℝ) (fun (x : α) ↦ δ * ‖g x‖) (s \ u) μ
Tactic: refine setIntegral_mono_on ?_ ?_ (hs.diff u_open.measurableSet) fun x 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 t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
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₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : norm.{u_2} (E := E) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ) ≤ 2 * δ
refine_1 : IntegrableOn (ε := ℝ) (fun (x : α) ↦ ‖φ i x • g x‖) (s \ u) μ
refine_2 : IntegrableOn (ε := ℝ) (fun (x : α) ↦ δ * ‖g x‖) (s \ u) μ
⊢ LE.le (α := ℝ) (∫ (x : α) in s \ u, ‖φ i x • g x‖ ∂μ) (∫ (x : α) in s \ u, δ * ‖g x‖ ∂μ)
have refine_3 : ∀ (x : α) (hx : x ∈ s \ u), ‖φ i x • g x‖ ≤ δ * ‖g x‖
Tactic: refine setIntegral_mono_on ?_ ?_ (hs.diff u_open.measurableSet) fun x 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 t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
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₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : norm.{u_2} (E := E) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ) ≤ 2 * δ
x : α
hx : x ∈ s \ u
⊢ ‖φ i x • g x‖ ≤ δ * ‖g x‖
have refine_3 : ‖φ i x‖ * ‖g x‖ ≤ δ * ‖g x‖
Tactic: rw [norm_smul]
-- 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 t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
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₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : norm.{u_2} (E := E) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ) ≤ 2 * δ
x : α
hx : x ∈ s \ u
⊢ ‖φ i x‖ * ‖g x‖ ≤ δ * ‖g x‖
have refine_3 : ‖φ i x‖ ≤ δ
Tactic: gcongr
-- 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 t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
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₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : norm.{u_2} (E := E) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ) ≤ 2 * δ
⊢ ∫ (x : α) in s \ u, δ * ‖g x‖ ∂μ ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ
have rw : δ * ∫ (a : α) in s \ u, ‖g a‖ ∂μ ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ
Tactic: rw [integral_const_mul]
-- 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 t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
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₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : norm.{u_2} (E := E) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ) ≤ 2 * δ
⊢ δ * ∫ (a : α) in s \ u, ‖g a‖ ∂μ ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ
have apply : (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖g a‖
Tactic: apply mul_le_mul_of_nonneg_left (setIntegral_mono_set hmg.norm _ _) δpos.le
-- 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 t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
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₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : norm.{u_2} (E := E) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ) ≤ 2 * δ
apply : (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖g a‖
⊢ δ * ∫ (a : α) in s \ u, ‖g a‖ ∂μ ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ
have apply₁ : s \ u ≤ᶠ[ae μ] s
Tactic: apply mul_le_mul_of_nonneg_left (setIntegral_mono_set hmg.norm _ _) δpos.le