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
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∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((Function.support (M := ℝ) fun (x : α) ↦ c x ^ n) ∩ s) : ℝ≥0∞)
have obtain : ∀ (u : Set α) (u_open : IsOpen[inst] u) (x₀_u : x₀ ∈ u) (hu : u ∩ s ⊆ c ⁻¹' Ioi 0),
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((Function.support (M := ℝ) fun (x : α) ↦ c x ^ n) ∩ s) : ℝ≥0∞)
Tactic: obtain ⟨u, u_open, x₀_u, hu⟩ : ∃ u : Set α, IsOpen u ∧ x₀ ∈ u ∧ u ∩ s ⊆ c ⁻¹' Ioi 0 :=
      _root_.continuousOn_iff.1 hc x₀ h₀ (Ioi (0 : ℝ)) isOpen_Ioi hnc₀
-- 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 : ℕ
u : Set α
u_open : IsOpen[inst] u
x₀_u : x₀ ∈ u
hu : u ∩ s ⊆ c ⁻¹' Ioi 0
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((Function.support (M := ℝ) fun (x : α) ↦ c x ^ n) ∩ s) : ℝ≥0∞)
have apply : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) ((Function.support (M := ℝ) fun (x : α) ↦ c x ^ n) ∩ s) : ℝ≥0∞)
Tactic: apply (hμ u u_open x₀_u).trans_le
-- 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 μ
J : ∀ (n : ℕ), (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ 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 P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
Tactic: have P : ∀ n, (0 : ℝ) < ∫ x in s, c x ^ n ∂μ := by
    intro n
    refine (setIntegral_pos_iff_support_of_nonneg_ae (J n) (I n)).2 ?_
    obtain ⟨u, u_open, x₀_u, hu⟩ : ∃ u : Set α, IsOpen u ∧ x₀ ∈ u ∧ u ∩ s ⊆ c ⁻¹' Ioi 0 :=
      _root_.continuousOn_iff.1 hc x₀ h₀ (Ioi (0 : ℝ)) isOpen_Ioi hnc₀
    apply (hμ u u_open x₀_u).trans_le
    exact measure_mono fun x hx => ⟨ne_of_gt (pow_pos (a := c x) (hu hx) _), hx.2⟩
-- 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
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
n : ℕ
⊢ Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
have rw : HMul.hMul (α := ℝ) (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ (∫ (a : α) in s, c a ^ n ∂μ) = 1
Tactic: rw [integral_const_mul, inv_mul_cancel₀ (P n).ne']
-- 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
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
n : ℕ
rw : HMul.hMul (α := ℝ) (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ (∫ (a : α) in s, c a ^ n ∂μ) = 1
⊢ Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
have rw₁ : Eq (α := ℝ) 1 1
Tactic: rw [integral_const_mul, inv_mul_cancel₀ (P n).ne']
-- 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 μ
J : ∀ (n : ℕ), (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ c x ^ n
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, 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 hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
Tactic: have hiφ : ∀ n, ∫ x in s, φ n x ∂μ = 1 := fun n => by
    rw [integral_const_mul, inv_mul_cancel₀ (P n).ne']
-- 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
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
⊢ ∃ (t : ℝ), 0 ≤ t ∧ t < c x₀ ∧ ∀ x ∈ s \ u, c x ≤ t
have inl : ∀ (h : s \ u = ∅), ∃ (t : ℝ), 0 ≤ t ∧ t < c x₀ ∧ ∀ x ∈ s \ u, c x ≤ t
Tactic: rcases eq_empty_or_nonempty (s \ u) with (h | h)
-- 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
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
inl : ∀ (h : s \ u = ∅), ∃ (t : ℝ), 0 ≤ t ∧ t < c x₀ ∧ ∀ x ∈ s \ u, c x ≤ t
⊢ ∃ (t : ℝ), 0 ≤ t ∧ t < c x₀ ∧ ∀ x ∈ s \ u, c x ≤ t
have inr : ∀ (h : (s \ u).Nonempty), ∃ (t : ℝ), 0 ≤ t ∧ t < c x₀ ∧ ∀ x ∈ s \ u, c x ≤ t
Tactic: rcases eq_empty_or_nonempty (s \ u) with (h | h)
-- 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
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
h : (s \ u).Nonempty
⊢ ∃ (t : ℝ), 0 ≤ t ∧ t < c x₀ ∧ ∀ x ∈ s \ u, c x ≤ t
have inr : ∀ (x : α) (hx : x ∈ s \ u) (h'x : ∀ y ∈ s \ u, c y ≤ c x), ∃ (t : ℝ), 0 ≤ t ∧ t < c x₀ ∧ ∀ x ∈ s \ u, c x ≤ t
Tactic: obtain ⟨x, hx, h'x⟩ : ∃ x ∈ s \ u, ∀ y ∈ s \ u, c y ≤ c x :=
        IsCompact.exists_isMaxOn (hs.diff u_open) h (hc.mono diff_subset)
-- 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
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
h : (s \ u).Nonempty
x : α
hx : x ∈ s \ u
h'x : ∀ y ∈ s \ u, c y ≤ c x
⊢ ∃ (t : ℝ), 0 ≤ t ∧ t < c x₀ ∧ ∀ x ∈ s \ u, c x ≤ t
have inr : x ≠ x₀
Tactic: refine ⟨c x, hnc x hx.1, h'c x hx.1 ?_, h'x⟩
-- 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
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
⊢ TendstoUniformlyOn φ 0 atTop (s \ u)
have obtain : ∀ (t : ℝ) (t_pos : 0 ≤ t) (tx₀ : t < c x₀) (ht : ∀ x ∈ s \ u, c x ≤ t), TendstoUniformlyOn φ 0 atTop (s \ u)
Tactic: obtain ⟨t, t_pos, tx₀, ht⟩ : ∃ t, 0 ≤ t ∧ t < c x₀ ∧ ∀ x ∈ s \ u, c x ≤ t := by
      rcases eq_empty_or_nonempty (s \ u) with (h | h)
      · exact
          ⟨0, le_rfl, hnc₀, by simp only [h, mem_empty_iff_false, IsEmpty.forall_iff, imp_true_iff]⟩
      obtain ⟨x, hx, h'x⟩ : ∃ x ∈ s \ u, ∀ y ∈ s \ u, c y ≤ c x :=
        IsCompact.exists_isMaxOn (hs.diff u_open) h (hc.mono diff_subset)
      refine ⟨c x, hnc x hx.1, h'c x hx.1 ?_, h'x⟩
      rintro rfl
      exact hx.2 x₀u
-- 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
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
⊢ TendstoUniformlyOn φ 0 atTop (s \ u)
have obtain : ∀ (t' : ℝ) (tt' : t < t') (t'x₀ : t' < c x₀), TendstoUniformlyOn φ 0 atTop (s \ u)
Tactic: obtain ⟨t', tt', t'x₀⟩ : ∃ t', t < t' ∧ t' < c x₀ := exists_between tx₀
-- 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 μ
J : ∀ (n : ℕ), (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ c x ^ n
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
t' : ℝ
tt' : t < t'
t'x₀ : t' < c x₀
⊢ TendstoUniformlyOn φ 0 atTop (s \ u)
have t'_pos : 0 < t'
Tactic: have t'_pos : 0 < t' := t_pos.trans_lt tt'
-- 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
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
t' : ℝ
tt' : t < t'
t'x₀ : t' < c x₀
t'_pos : 0 < t'
⊢ TendstoUniformlyOn φ 0 atTop (s \ u)
have obtain : ∀ (v : Set α) (v_open : IsOpen[inst] v) (x₀_v : x₀ ∈ v) (hv : v ∩ s ⊆ c ⁻¹' Ioi t'),
  TendstoUniformlyOn φ 0 atTop (s \ u)
Tactic: obtain ⟨v, v_open, x₀_v, hv⟩ : ∃ v : Set α, IsOpen v ∧ x₀ ∈ v ∧ v ∩ s ⊆ c ⁻¹' Ioi t' :=
      _root_.continuousOn_iff.1 hc x₀ h₀ (Ioi t') isOpen_Ioi t'x₀
-- 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
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
t' : ℝ
tt' : t < t'
t'x₀ : t' < c x₀
t'_pos : 0 < t'
v : Set α
v_open : IsOpen[inst] v
x₀_v : x₀ ∈ v
hv : v ∩ s ⊆ c ⁻¹' Ioi t'
n : ℕ
x : α
hx : x ∈ s \ u
⊢ LE.le (α := ℝ) (∫ (x : α) in v ∩ s, t' ^ n ∂μ) (∫ (y : α) in v ∩ s, c y ^ n ∂μ)
have apply : IntegrableOn (ε := ℝ) (fun (x : α) ↦ t' ^ n) (v ∩ s) μ
Tactic: apply setIntegral_mono_on _ _ (v_open.measurableSet.inter hs.measurableSet) _
-- 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
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
t' : ℝ
tt' : t < t'
t'x₀ : t' < c x₀
t'_pos : 0 < t'
v : Set α
v_open : IsOpen[inst] v
x₀_v : x₀ ∈ v
hv : v ∩ s ⊆ c ⁻¹' Ioi t'
n : ℕ
x : α
hx : x ∈ s \ u
apply : IntegrableOn (ε := ℝ) (fun (x : α) ↦ t' ^ n) (v ∩ s) μ
⊢ LE.le (α := ℝ) (∫ (x : α) in v ∩ s, t' ^ n ∂μ) (∫ (y : α) in v ∩ s, c y ^ n ∂μ)
have apply₁ : IntegrableOn (ε := ℝ) (fun (x : α) ↦ c x ^ n) (v ∩ s) μ
Tactic: apply setIntegral_mono_on _ _ (v_open.measurableSet.inter hs.measurableSet) _
-- 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
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
t' : ℝ
tt' : t < t'
t'x₀ : t' < c x₀
t'_pos : 0 < t'
v : Set α
v_open : IsOpen[inst] v
x₀_v : x₀ ∈ v
hv : v ∩ s ⊆ c ⁻¹' Ioi t'
n : ℕ
x : α
hx : x ∈ s \ u
apply : IntegrableOn (ε := ℝ) (fun (x : α) ↦ t' ^ n) (v ∩ s) μ
apply₁ : IntegrableOn (ε := ℝ) (fun (x : α) ↦ c x ^ n) (v ∩ s) μ
⊢ LE.le (α := ℝ) (∫ (x : α) in v ∩ s, t' ^ n ∂μ) (∫ (y : α) in v ∩ s, c y ^ n ∂μ)
have apply₂ : ∀ x ∈ v ∩ s, t' ^ n ≤ c x ^ n
Tactic: apply setIntegral_mono_on _ _ (v_open.measurableSet.inter hs.measurableSet) _