awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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₀
rw : x₀ ∈ closure[inst] s
⊢ x₀ ∈ s

Tactic:
rw [← hs.isClosed.closure_eq]

Premises used: IsClosed.closure_eq, IsCompact.isClosed
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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₀ ∈ closure[inst] s

Tactic:
closure_mono interior_subset h₀

Premises used: interior_subset, closure_mono
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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₀ ∈ closure[inst] s

Tactic:
exact closure_mono interior_subset h₀

Premises used: interior_subset, closure_mono
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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

Tactic:
have : x₀ ∈ s := by rw [← hs.isClosed.closure_eq]; exact closure_mono interior_subset h₀
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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_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∞)
⊢ Tendsto
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ (∫ (x : α) in s, c x ^ n • g x ∂μ))
    atTop (𝓝 (g x₀))

Tactic:
apply
    tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_measure_nhdsWithin_pos hs _ hc
      h'c hnc hnc₀ this hmg hcg

Premises used: tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_measure_nhdsWithin_pos
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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 ∩ interior s) : ℝ≥0∞)

Tactic:
(u_open.inter isOpen_interior).measure_pos μ (_root_.mem_closure_iff.1 h₀ u u_open x₀_u)

Premises used: mem_closure_iff, isOpen_interior, IsOpen.measure_pos, IsOpen.inter, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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
h : interior s ⊆ s
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ interior s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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
⊢ interior s ⊆ s

Tactic:
apply interior_subset

Premises used: interior_subset
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥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

Premises used: mem_closure_iff, isOpen_interior, IsOpen.measure_pos, Inter.inter, interior, IsOpen.inter, Iff.mp, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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
rw : x₀ ∈ closure[inst] s
⊢ x₀ ∈ s

Tactic:
rw [← hs.isClosed.closure_eq]

Premises used: IsClosed.closure_eq, IsCompact.isClosed
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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₀ ∈ closure[inst] s

Tactic:
closure_mono interior_subset h₀

Premises used: interior_subset, closure_mono
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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₀ ∈ closure[inst] s

Tactic:
exact closure_mono interior_subset h₀

Premises used: interior_subset, closure_mono
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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
⊢ Integrable φ μ

Tactic:
have I : Integrable φ μ := integrable_of_integral_eq_one h'φ
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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 μ
hcg : Tendsto g (𝓝 0) (𝓝 (g 0))
⊢ Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g x ∂μ) atTop (𝓝 (g 0))

Tactic:
apply tendsto_integral_peak_smul_of_integrable_of_tendsto (t := closedBall 0 1) (x₀ := 0)

Premises used: tendsto_integral_peak_smul_of_integrable_of_tendsto
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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 φ μ
⊢ MeasurableSet.{u_4} (α := F) (closedBall 0 1)

Tactic:
isClosed_closedBall.measurableSet

Premises used: Metric.isClosed_closedBall, IsClosed.measurableSet
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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 φ μ
⊢ MeasurableSet.{u_4} (α := F) (closedBall 0 1)

Tactic:
exact isClosed_closedBall.measurableSet

Premises used: Metric.isClosed_closedBall, IsClosed.measurableSet
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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 φ μ
⊢ Membership.mem (γ := Filter F) (𝓝 0) (closedBall 0 1)

Tactic:
closedBall_mem_nhds _ zero_lt_one

Premises used: Metric.closedBall_mem_nhds, zero_lt_one
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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 φ μ
⊢ Membership.mem (γ := Filter F) (𝓝 0) (closedBall 0 1)

Tactic:
exact closedBall_mem_nhds _ zero_lt_one

Premises used: Metric.closedBall_mem_nhds, zero_lt_one
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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 φ μ
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set F) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(isCompact_closedBall 0 1).measure_ne_top

Premises used: ProperSpace.isCompact_closedBall, OfNat.ofNat, IsCompact.measure_ne_top
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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 φ μ
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set F) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact (isCompact_closedBall 0 1).measure_ne_top

Premises used: ProperSpace.isCompact_closedBall, OfNat.ofNat, IsCompact.measure_ne_top
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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 : ℝ
h₁ : ∀ (hc : 0 ≤ c) (x : F), 0 ≤ c ^ finrank ℝ F * φ (c • x)
⊢ Membership.mem (γ := Set ℝ) (Ici 0) c → ∀ (x : F), 0 ≤ c ^ finrank ℝ F * φ (c • x)

Tactic:
(hc : 0 ≤ c)
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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 : ℝ
hc : 0 ≤ c
x : F
⊢ 0 ≤ c ^ finrank ℝ F

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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 φ μ
h₁ :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) (Ici 0) x →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (i : ℝ) ↦ ∀ (x : F), 0 ≤ i ^ finrank ℝ F * φ (i • x)) x} x}
      a
h₂ : ∀ (a : ℝ), Membership.mem (γ := Set ℝ) (Ici 0) a → ∀ (x : F), 0 ≤ a ^ finrank ℝ F * φ (a • x)
h₃ : ∀ (c : ℝ) (hc : 0 ≤ c) (x : F), 0 ≤ c ^ finrank ℝ F * φ (c • x)
⊢ ∀ᶠ (i : ℝ) in atTop, ∀ (x : F), 0 ≤ i ^ finrank ℝ F * φ (i • x)

Tactic:
filter_upwards [Ici_mem_atTop 0] with c (hc : 0 ≤ c) x using mul_nonneg (by positivity) (hφ _)

Premises used: mul_nonneg, Filter.Ici_mem_atTop, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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 φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
apply : ∀ (ε : ℝ) (εpos : ε > 0), ∀ᶠ (n : ℝ) in atTop, ∀ x ∈ uᶜ, dist (0 x) (n ^ finrank ℝ F * φ (n • x)) < ε
⊢ TendstoUniformlyOn (β := ℝ) (fun (i : ℝ) (x : F) ↦ i ^ finrank ℝ F * φ (i • x)) 0 atTop uᶜ

Tactic:
apply tendstoUniformlyOn_iff.2 (fun ε εpos ↦ ?_)

Premises used: Iff.mpr, Metric.tendstoUniformlyOn_iff
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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 φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
⊢ ∃ δ > 0, ball 0 δ ⊆ u

Tactic:
Metric.isOpen_iff.1 u_open _ hu

Premises used: Metric.isOpen_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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 φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
obtain :
  ∀ (δ : ℝ) (δpos : δ > 0) (h'u : ball 0 δ ⊆ u),
    ∀ᶠ (n : ℝ) in atTop, ∀ x ∈ uᶜ, dist (0 x) (n ^ finrank ℝ F * φ (n • x)) < ε
⊢ ∀ᶠ (n : ℝ) in atTop, ∀ x ∈ uᶜ, dist (0 x) (n ^ finrank ℝ F * φ (n • x)) < ε

Tactic:
obtain ⟨δ, δpos, h'u⟩ : ∃ δ > 0, ball 0 δ ⊆ u := Metric.isOpen_iff.1 u_open _ hu

Premises used: Metric.isOpen_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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 φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
⊢ δ ^ finrank ℝ F * ε > 0

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
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 φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
rcases :
  ∀ (M : ℝ)
    (hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε),
    ∃ M > 0, ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
⊢ ∃ M > 0, ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε

Tactic:
rcases (hasBasis_cobounded_compl_closedBall (0 : F)).eventually_iff.1
        ((tendsto_order.1 h).2 (δ ^ finrank ℝ F * ε) (by positivity)) with ⟨M, -, hM⟩

Premises used: Metric.hasBasis_cobounded_compl_closedBall, Real, HMul.hMul, tendsto_order, HPow.hPow, And.right, Iff.mp, Filter.HasBasis.eventually_iff, OfNat.ofNat, Module.finrank