awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
A : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 atTop (s \ u)
⊢ Tendsto (fun (i : ℕ) ↦ ∫ (x : α) in s, φ i x • g x ∂μ) atTop (𝓝 (g x₀))
have B : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (x : α) in s, φ i x ∂μ) atTop (𝓝 1)
Tactic: have B : Tendsto (fun i ↦ ∫ (x : α) in s, φ i x ∂μ) atTop (𝓝 1) :=
      tendsto_const_nhds.congr (fun n ↦ (hiφ n).symm)
-- 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
A : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 atTop (s \ u)
B : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (x : α) in s, φ i x ∂μ) atTop (𝓝 1)
⊢ Tendsto (fun (i : ℕ) ↦ ∫ (x : α) in s, φ i x • g x ∂μ) atTop (𝓝 (g x₀))
have C : ∀ᶠ (i : ℕ) in atTop, AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ φ i x) (μ.restrict s)
Tactic: have C : ∀ᶠ (i : ℕ) in atTop, AEStronglyMeasurable (fun x ↦ φ i x) (μ.restrict s) := by
      apply Eventually.of_forall (fun n ↦ ((I n).const_mul _).aestronglyMeasurable)
-- 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
A : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 atTop (s \ u)
⊢ Tendsto
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ (∫ (x : α) in s, c x ^ n • g x ∂μ))
    atTop (𝓝 (g x₀))
have this : Tendsto (fun (i : ℕ) ↦ ∫ (x : α) in s, φ i x • g x ∂μ) atTop (𝓝 (g x₀))
Tactic: have : Tendsto (fun i : ℕ => ∫ x : α in s, φ i x • g x ∂μ) atTop (𝓝 (g x₀)) := by
    have B : Tendsto (fun i ↦ ∫ (x : α) in s, φ i x ∂μ) atTop (𝓝 1) :=
      tendsto_const_nhds.congr (fun n ↦ (hiφ n).symm)
    have C : ∀ᶠ (i : ℕ) in atTop, AEStronglyMeasurable (fun x ↦ φ i x) (μ.restrict s) := by
      apply Eventually.of_forall (fun n ↦ ((I n).const_mul _).aestronglyMeasurable)
    exact tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto hs.measurableSet
      hs.measurableSet (Subset.rfl) (self_mem_nhdsWithin)
      hs.measure_lt_top.ne (Eventually.of_forall hnφ) A B C hmg hcg
-- 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
A : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 atTop (s \ u)
this : Tendsto (fun (i : ℕ) ↦ ∫ (x : α) in s, φ i x • g x ∂μ) atTop (𝓝 (g 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 h : ∀ (x : ℕ),
  HSMul.hSMul (α := ℝ) (β := E) (∫ (x_1 : α) in s, c x_1 ^ x ∂μ)⁻¹ (∫ (x_1 : α) in s, c x_1 ^ x • g x_1 ∂μ) =
    ∫ (x_1 : α) in s, φ x x_1 • g x_1 ∂μ
Tactic: convert! this
-- 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
A : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 atTop (s \ u)
this : Tendsto (fun (i : ℕ) ↦ ∫ (x : α) in s, φ i x • g x ∂μ) atTop (𝓝 (g x₀))
x : ℕ
h :
  HSMul.hSMul (α := ℝ) (β := E) (∫ (x_1 : α) in s, c x_1 ^ x ∂μ)⁻¹ (∫ (x_1 : α) in s, c x_1 ^ x • g x_1 ∂μ) =
    ∫ (x_1 : α) in s, ((∫ (x_2 : α) in s, c x_2 ^ x ∂μ)⁻¹ * c x_1 ^ x) • g x_1 ∂μ
⊢ HSMul.hSMul (α := ℝ) (β := E) (∫ (x_1 : α) in s, c x_1 ^ x ∂μ)⁻¹ (∫ (x_1 : α) in s, c x_1 ^ x • g x_1 ∂μ) =
    ∫ (x_1 : α) in s, φ x x_1 • g x_1 ∂μ
have h₁ : HSMul.hSMul (α := ℝ) (β := E) (∫ (x_1 : α) in s, c x_1 ^ x ∂μ)⁻¹ (∫ (x_1 : α) in s, c x_1 ^ x • g x_1 ∂μ) =
  ∫ (x_1 : α) in s, HSMul.hSMul (α := ℝ) (∫ (x_2 : α) in s, c x_2 ^ x ∂μ)⁻¹ (c x_1 ^ x • g x_1) ∂μ
Tactic: simp_rw [φ, ← smul_smul, integral_smul]
-- 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 μ
inst_7 : μ.IsOpenPosMeasure
hs : IsCompact s
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₀ ∈ closure[inst] (interior s)
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
⊢ x₀ ∈ s
have rw : x₀ ∈ closure[inst] s
Tactic: rw [← hs.isClosed.closure_eq]
-- 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 μ
inst_7 : μ.IsOpenPosMeasure
hs : IsCompact s
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₀ ∈ closure[inst] (interior s)
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s 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 this : x₀ ∈ s
Tactic: have : x₀ ∈ s := by rw [← hs.isClosed.closure_eq]; exact closure_mono interior_subset 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 μ
inst_7 : μ.IsOpenPosMeasure
hs : IsCompact s
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₀ ∈ closure[inst] (interior s)
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
this : x₀ ∈ 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 tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_measure_nhdsWithin_pos : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
Tactic: apply
    tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_measure_nhdsWithin_pos hs _ hc
      h'c hnc hnc₀ this hmg hcg
-- 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 μ
inst_7 : μ.IsOpenPosMeasure
hs : IsCompact s
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₀ ∈ closure[inst] (interior s)
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
this : x₀ ∈ s
u : Set α
u_open : IsOpen[inst] u
x₀_u : x₀ ∈ u
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ interior s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
have h : interior s ⊆ s
Tactic: gcongr
-- 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 μ
inst_7 : μ.IsOpenPosMeasure
hs : IsCompact s
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₀ ∈ closure[inst] (interior s)
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
this : x₀ ∈ s
u : Set α
u_open : IsOpen[inst] u
x₀_u : x₀ ∈ u
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
have μ₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ interior s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
Tactic: calc
    0 < μ (u ∩ interior s) :=
      (u_open.inter isOpen_interior).measure_pos μ (_root_.mem_closure_iff.1 h₀ u u_open x₀_u)
    _ ≤ μ (u ∩ s) := by gcongr; apply interior_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 μ
inst_7 : μ.IsOpenPosMeasure
hs : IsCompact s
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₀ ∈ closure[inst] (interior s)
hmg : ContinuousOn g s
⊢ x₀ ∈ s
have rw : x₀ ∈ closure[inst] s
Tactic: rw [← hs.isClosed.closure_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
⊢ Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g x ∂μ) atTop (𝓝 (g 0))
have I : Integrable φ μ
Tactic: have I : Integrable φ μ := integrable_of_integral_eq_one h'φ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
⊢ Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g x ∂μ) atTop (𝓝 (g 0))
have ht : MeasurableSet.{u_4} (α := F) (closedBall 0 1)
Tactic: apply tendsto_integral_peak_smul_of_integrable_of_tendsto (t := closedBall 0 1) (x₀ := 0)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
ht : MeasurableSet.{u_4} (α := F) (closedBall 0 1)
⊢ Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g x ∂μ) atTop (𝓝 (g 0))
have h'ts : Membership.mem (γ := Filter F) (𝓝 0) (closedBall 0 1)
Tactic: apply tendsto_integral_peak_smul_of_integrable_of_tendsto (t := closedBall 0 1) (x₀ := 0)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
ht : MeasurableSet.{u_4} (α := F) (closedBall 0 1)
h'ts : Membership.mem (γ := Filter F) (𝓝 0) (closedBall 0 1)
⊢ Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g x ∂μ) atTop (𝓝 (g 0))
have h't : Ne (α := ℝ≥0∞) ((μ : (a : Set F) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply tendsto_integral_peak_smul_of_integrable_of_tendsto (t := closedBall 0 1) (x₀ := 0)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
ht : MeasurableSet.{u_4} (α := F) (closedBall 0 1)
h'ts : Membership.mem (γ := Filter F) (𝓝 0) (closedBall 0 1)
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set F) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g x ∂μ) atTop (𝓝 (g 0))
have hnφ : ∀ᶠ (i : ℝ) in atTop, ∀ (x : F), 0 ≤ i ^ finrank ℝ F * φ (i • x)
Tactic: apply tendsto_integral_peak_smul_of_integrable_of_tendsto (t := closedBall 0 1) (x₀ := 0)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
ht : MeasurableSet.{u_4} (α := F) (closedBall 0 1)
h'ts : Membership.mem (γ := Filter F) (𝓝 0) (closedBall 0 1)
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set F) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) (∞ : ℝ≥0∞)
hnφ : ∀ᶠ (i : ℝ) in atTop, ∀ (x : F), 0 ≤ i ^ finrank ℝ F * φ (i • x)
⊢ Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g x ∂μ) atTop (𝓝 (g 0))
have hlφ : ∀ (u : Set F),
  IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u →
    0 ∈ u → TendstoUniformlyOn (β := ℝ) (fun (i : ℝ) (x : F) ↦ i ^ finrank ℝ F * φ (i • x)) 0 atTop uᶜ
Tactic: apply tendsto_integral_peak_smul_of_integrable_of_tendsto (t := closedBall 0 1) (x₀ := 0)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
ht : MeasurableSet.{u_4} (α := F) (closedBall 0 1)
h'ts : Membership.mem (γ := Filter F) (𝓝 0) (closedBall 0 1)
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set F) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) (∞ : ℝ≥0∞)
hnφ : ∀ᶠ (i : ℝ) in atTop, ∀ (x : F), 0 ≤ i ^ finrank ℝ F * φ (i • x)
hlφ :
  ∀ (u : Set F),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u →
      0 ∈ u → TendstoUniformlyOn (β := ℝ) (fun (i : ℝ) (x : F) ↦ i ^ finrank ℝ F * φ (i • x)) 0 atTop uᶜ
⊢ Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g x ∂μ) atTop (𝓝 (g 0))
have hiφ : Tendsto (β := ℝ) (fun (i : ℝ) ↦ ∫ (x : F) in closedBall 0 1, i ^ finrank ℝ F * φ (i • x) ∂μ) atTop (𝓝 1)
Tactic: apply tendsto_integral_peak_smul_of_integrable_of_tendsto (t := closedBall 0 1) (x₀ := 0)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
ht : MeasurableSet.{u_4} (α := F) (closedBall 0 1)
h'ts : Membership.mem (γ := Filter F) (𝓝 0) (closedBall 0 1)
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set F) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) (∞ : ℝ≥0∞)
hnφ : ∀ᶠ (i : ℝ) in atTop, ∀ (x : F), 0 ≤ i ^ finrank ℝ F * φ (i • x)
hlφ :
  ∀ (u : Set F),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u →
      0 ∈ u → TendstoUniformlyOn (β := ℝ) (fun (i : ℝ) (x : F) ↦ i ^ finrank ℝ F * φ (i • x)) 0 atTop uᶜ
hiφ : Tendsto (β := ℝ) (fun (i : ℝ) ↦ ∫ (x : F) in closedBall 0 1, i ^ finrank ℝ F * φ (i • x) ∂μ) atTop (𝓝 1)
⊢ Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g x ∂μ) atTop (𝓝 (g 0))
have h'iφ : ∀ᶠ (i : ℝ) in atTop, AEStronglyMeasurable (β := ℝ) (fun (x : F) ↦ i ^ finrank ℝ F * φ (i • x)) μ
Tactic: apply tendsto_integral_peak_smul_of_integrable_of_tendsto (t := closedBall 0 1) (x₀ := 0)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
ht : MeasurableSet.{u_4} (α := F) (closedBall 0 1)
h'ts : Membership.mem (γ := Filter F) (𝓝 0) (closedBall 0 1)
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set F) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) (∞ : ℝ≥0∞)
hnφ : ∀ᶠ (i : ℝ) in atTop, ∀ (x : F), 0 ≤ i ^ finrank ℝ F * φ (i • x)
hlφ :
  ∀ (u : Set F),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u →
      0 ∈ u → TendstoUniformlyOn (β := ℝ) (fun (i : ℝ) (x : F) ↦ i ^ finrank ℝ F * φ (i • x)) 0 atTop uᶜ
hiφ : Tendsto (β := ℝ) (fun (i : ℝ) ↦ ∫ (x : F) in closedBall 0 1, i ^ finrank ℝ F * φ (i • x) ∂μ) atTop (𝓝 1)
h'iφ : ∀ᶠ (i : ℝ) in atTop, AEStronglyMeasurable (β := ℝ) (fun (x : F) ↦ i ^ finrank ℝ F * φ (i • x)) μ
hmg : Integrable g μ
⊢ Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g x ∂μ) atTop (𝓝 (g 0))
have hcg : Tendsto g (𝓝 0) (𝓝 (g 0))
Tactic: apply tendsto_integral_peak_smul_of_integrable_of_tendsto (t := closedBall 0 1) (x₀ := 0)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
c : ℝ
⊢ Membership.mem (γ := Set ℝ) (Ici 0) c → ∀ (x : F), 0 ≤ c ^ finrank ℝ F * φ (c • x)
have h₁ : ∀ (hc : 0 ≤ c) (x : F), 0 ≤ c ^ finrank ℝ F * φ (c • x)
Tactic: (hc : 0 ≤ c)