awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M < c * δ
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
⊢ Membership.mem (γ := Set F) (closedBall 0 M)ᶜ (c • x)
have a : M < c * ‖x‖
Tactic: simp only [mem_compl_iff, mem_closedBall, dist_zero_right, norm_smul, Real.norm_eq_abs,
          abs_of_nonneg cpos.le, not_le]
-- 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 φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M < c * δ
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
⊢ c * δ ≤ c * ‖x‖
have ha : 0 ≤ c
Tactic: gcongr
-- 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 φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
⊢ δ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) < δ ^ finrank ℝ F * ε
have δ₁ : δ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) ≤ ‖x‖ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x))
Tactic: calc
      δ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x))
      _ ≤ ‖x‖ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) := by
        gcongr; exact mul_nonneg (by positivity) (hφ _)
      _ = ‖c • x‖ ^ finrank ℝ F * φ (c • x) := by
        simp [norm_smul, abs_of_pos cpos, mul_pow]; ring
      _ < δ ^ finrank ℝ F * ε := by
        apply hM
        rw [div_lt_iff₀ δpos] at hc
        simp only [mem_compl_iff, mem_closedBall, dist_zero_right, norm_smul, Real.norm_eq_abs,
          abs_of_nonneg cpos.le, not_le]
        exact hc.trans_le (by gcongr)
-- 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 φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
δ₁ : δ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) ≤ ‖x‖ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x))
⊢ δ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) < δ ^ finrank ℝ F * ε
have δ₂ : ‖x‖ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) = ‖c • x‖ ^ finrank ℝ F * φ (c • x)
Tactic: calc
      δ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x))
      _ ≤ ‖x‖ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) := by
        gcongr; exact mul_nonneg (by positivity) (hφ _)
      _ = ‖c • x‖ ^ finrank ℝ F * φ (c • x) := by
        simp [norm_smul, abs_of_pos cpos, mul_pow]; ring
      _ < δ ^ finrank ℝ F * ε := by
        apply hM
        rw [div_lt_iff₀ δpos] at hc
        simp only [mem_compl_iff, mem_closedBall, dist_zero_right, norm_smul, Real.norm_eq_abs,
          abs_of_nonneg cpos.le, not_le]
        exact hc.trans_le (by gcongr)
-- 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 φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
δ₁ : δ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) ≤ ‖x‖ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x))
δ₂ : ‖x‖ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) = ‖c • x‖ ^ finrank ℝ F * φ (c • x)
⊢ δ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) < δ ^ finrank ℝ F * ε
have δ₃ : ‖c • x‖ ^ finrank ℝ F * φ (c • x) < δ ^ finrank ℝ F * ε
Tactic: calc
      δ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x))
      _ ≤ ‖x‖ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) := by
        gcongr; exact mul_nonneg (by positivity) (hφ _)
      _ = ‖c • x‖ ^ finrank ℝ F * φ (c • x) := by
        simp [norm_smul, abs_of_pos cpos, mul_pow]; ring
      _ < δ ^ finrank ℝ F * ε := by
        apply hM
        rw [div_lt_iff₀ δpos] at hc
        simp only [mem_compl_iff, mem_closedBall, dist_zero_right, norm_smul, Real.norm_eq_abs,
          abs_of_nonneg cpos.le, not_le]
        exact hc.trans_le (by gcongr)
-- 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) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1)
have rw : Tendsto (β := ℝ) (fun (c : ℝ) ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 (∫ (x : F), φ x ∂μ))
Tactic: rw [← h'φ]
-- 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
I : Integrable φ μ
⊢ Tendsto (β := ℝ) (fun (i : ℝ) ↦ ∫ (x : F) in closedBall 0 1, i ^ finrank ℝ F * φ (i • x) ∂μ) atTop (𝓝 1)
have this : Tendsto (β := ℝ) (fun (c : ℝ) ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1)
Tactic: have : Tendsto (fun c ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1) := by
      rw [← h'φ]
      exact (aecover_closedBall tendsto_id).integral_tendsto_of_countably_generated I
-- 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 φ μ
this : Tendsto (β := ℝ) (fun (c : ℝ) ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1)
⊢ Tendsto (β := ℝ) (fun (i : ℝ) ↦ ∫ (x : F) in closedBall 0 1, i ^ finrank ℝ F * φ (i • x) ∂μ) atTop (𝓝 1)
have hiφ : EventuallyEq (β := ℝ) atTop (fun (c : ℝ) ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) fun (i : ℝ) ↦
  ∫ (x : F) in closedBall 0 1, i ^ finrank ℝ F * φ (i • x) ∂μ
Tactic: apply this.congr'
-- 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 φ μ
this : Tendsto (β := ℝ) (fun (c : ℝ) ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1)
c : ℝ
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) c →
    Eq (α := ℝ) (∫ (x : F) in closedBall 0 c, φ x ∂μ) (∫ (x : F) in closedBall 0 1, c ^ finrank ℝ F * φ (c • x) ∂μ)
have h₁ : ∀ (hc : 0 < c),
  Eq (α := ℝ) (∫ (x : F) in closedBall 0 c, φ x ∂μ) (∫ (x : F) in closedBall 0 1, c ^ finrank ℝ F * φ (c • x) ∂μ)
Tactic: (hc : 0 < c)
-- 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 φ μ
this : Tendsto (β := ℝ) (fun (c : ℝ) ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1)
⊢ EventuallyEq (β := ℝ) atTop (fun (c : ℝ) ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) fun (i : ℝ) ↦
    ∫ (x : F) in closedBall 0 1, i ^ finrank ℝ F * φ (i • x) ∂μ
have h₁ : ∀ (c : ℝ) (hc : 0 < c),
  Eq (α := ℝ) (∫ (x : F) in closedBall 0 c, φ x ∂μ) (∫ (x : F) in closedBall 0 1, c ^ finrank ℝ F * φ (c • x) ∂μ)
Tactic: filter_upwards [Ioi_mem_atTop 0] with c (hc : 0 < c)
-- 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 φ μ
this : Tendsto (β := ℝ) (fun (c : ℝ) ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1)
c : ℝ
hc : 0 < c
⊢ Eq (α := ℝ) (∫ (x : F) in closedBall 0 c, φ x ∂μ) (∫ (x : F) in closedBall 0 1, c ^ finrank ℝ F * φ (c • x) ∂μ)
have h₁ : ∫ (x : F) in closedBall 0 c, φ x ∂μ =
  HMul.hMul (α := ℝ) 1 (∫ (x : F) in closedBall (HSMul.hSMul (β := F) c 0) (‖c‖ * 1), φ x ∂μ)
Tactic: rw [integral_const_mul, setIntegral_comp_smul_of_pos _ _ _ hc, smul_eq_mul, ← mul_assoc,
      mul_inv_cancel₀ (by positivity), _root_.smul_closedBall _ _ zero_le_one]
-- 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 ℝ) (Ioi 0) c → AEStronglyMeasurable (β := ℝ) (fun (x : F) ↦ c ^ finrank ℝ F * φ (c • x)) μ
have h₁ : ∀ (hc : 0 < c), AEStronglyMeasurable (β := ℝ) (fun (x : F) ↦ c ^ finrank ℝ F * φ (c • x)) μ
Tactic: (hc : 0 < c)
-- 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 φ μ
⊢ ∀ᶠ (i : ℝ) in atTop, AEStronglyMeasurable (β := ℝ) (fun (x : F) ↦ i ^ finrank ℝ F * φ (i • x)) μ
have h₁ : ∀ (c : ℝ) (hc : 0 < c), AEStronglyMeasurable (β := ℝ) (fun (x : F) ↦ c ^ finrank ℝ F * φ (c • x)) μ
Tactic: filter_upwards [Ioi_mem_atTop 0] with c (hc : 0 < c)
-- 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
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : (x : F) → E := fun (x : F) ↦ g (x₀ - x)
⊢ Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ) atTop (𝓝 (g x₀))
have If : Integrable f μ
Tactic: have If : Integrable f μ := by simpa [f, sub_eq_add_neg] using (hg.comp_add_left x₀).comp_neg
-- 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
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : (x : F) → E := fun (x : F) ↦ g (x₀ - x)
If : Integrable f μ
⊢ Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • f x ∂μ) atTop (𝓝 (f 0))
have apply : ContinuousAt f 0
Tactic: apply tendsto_integral_comp_smul_smul_of_integrable hφ h'φ h If
-- 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
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : (x : F) → E := fun (x : F) ↦ g (x₀ - x)
If : Integrable f μ
⊢ ContinuousAt f 0
have A : ContinuousAt g (x₀ - 0)
Tactic: have A : ContinuousAt g (x₀ - 0) := by simpa using h'g
-- 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
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : (x : F) → E := fun (x : F) ↦ g (x₀ - x)
If : Integrable f μ
⊢ Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ) atTop (𝓝 (g x₀))
have this : Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • f x ∂μ) atTop (𝓝 (f 0))
Tactic: have : Tendsto (fun (c : ℝ) ↦ ∫ x, (c ^ (finrank ℝ F) * φ (c • x)) • f x ∂μ)
      atTop (𝓝 (f 0)) := by
    apply tendsto_integral_comp_smul_smul_of_integrable hφ h'φ h If
    have A : ContinuousAt g (x₀ - 0) := by simpa using h'g
    exact A.comp <| by fun_prop
-- 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
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : (x : F) → E := fun (x : F) ↦ g (x₀ - x)
If : Integrable f μ
this : Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • f x ∂μ) atTop (𝓝 (f 0))
⊢ Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ) atTop (𝓝 (g x₀))
have this₁ : Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ) atTop (𝓝 (g x₀))
Tactic: simp only [f, sub_zero] at this
Cleared hypotheses: this
-- 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
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : (x : F) → E := fun (x : F) ↦ g (x₀ - x)
If : Integrable f μ
this : Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ) atTop (𝓝 (g x₀))
⊢ Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ) atTop (𝓝 (g x₀))
have h₁ : ∀ (c : ℝ),
  Eq.{u_2 + 1} (α := E) (∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ)
    (∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ)
Tactic: convert! this using 2 with c
-- 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
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : (x : F) → E := fun (x : F) ↦ g (x₀ - x)
If : Integrable f μ
this : Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ) atTop (𝓝 (g x₀))
c : ℝ
| ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ
have rw : ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ + -x))) • g (x₀ - (x₀ + -x)) ∂μ
Tactic: rw [← integral_add_left_eq_self x₀ (μ := μ)
    (f := fun x ↦ (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x)), ← integral_neg_eq_self]
-- 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
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : (x : F) → E := fun (x : F) ↦ g (x₀ - x)
If : Integrable f μ
this : Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ) atTop (𝓝 (g x₀))
c : ℝ
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ)
    (∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ)
have h₁ : Eq.{u_2 + 1} (α := E) (∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ)
  (∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ + -x))) • g (x₀ - (x₀ + -x)) ∂μ)
Tactic: conv_rhs => rw [← integral_add_left_eq_self x₀ (μ := μ)
    (f := fun x ↦ (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x)), ← integral_neg_eq_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (hypothesis)
Goal:
𝕜 : Type u_1
inst : NormedCommRing 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] {f : (i : Fin n) → E i → 𝕜} (hf : ∀ (i : Fin n), Integrable (f i) (μ i)),
    Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin n) → E i) ↦ ∏ i : Fin n, f i (x i)) (Measure.pi (α := E) μ)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst_1 : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) (μ i)
⊢ Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin (n + 1)) → E i) ↦ ∏ i : Fin (n + 1), f i (x i))
    (Measure.pi (α := E) μ)
have this : MeasurePreserving (α := E 0 × ((j : Fin n) → E (Fin.succAbove 0 j)))
  (⇑(MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove E 0)) :
    (a : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) → (j : Fin (n + 1)) → E j)
  (Measure.prod (μ 0)
    (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))
  (Measure.pi (α := E) μ)
Tactic: have := ((measurePreserving_piFinSuccAbove μ 0).symm)