awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
apply :
  Subset (α := Set ℝ)
    {a : ℝ |
      ∀ᶠ (n : ℝ) in
        map
          (fun (n : ℕ) ↦
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
          atTop,
        n ≤ a}
    {a : ℝ |
      ∀ᶠ (n : ℝ) in
        map (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
          atTop,
        n ≤ a}
⊢ LE.le (α := ℝ)
    (limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop)
    (limsup
      (fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop)
have apply₁ : BddBelow (α := ℝ)
  {a : ℝ |
    ∀ᶠ (n : ℝ) in
      map (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
        atTop,
      n ≤ a}
Tactic: apply csInf_le_csInf _ (μ_nonempty μ hs_le ψ)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
b : ℝ
hb :
  Membership.mem (γ := Set ℝ)
    {a : ℝ |
      ∀ᶠ (n : ℝ) in
        map
          (fun (n : ℕ) ↦
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
          atTop,
        n ≤ a}
    b
⊢ Membership.mem (γ := Set ℝ)
    {a : ℝ |
      ∀ᶠ (n : ℝ) in
        map (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
          atTop,
        n ≤ a}
    b
have simp : ∀
  (hb :
    ∃ (a : ℕ),
      ∀ (b_1 : ℕ),
        a ≤ b_1 →
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b_1)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤ b),
  ∃ (a : ℕ),
    ∀ (b_1 : ℕ),
      a ≤ b_1 → HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ b_1)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤ b
Tactic: simp only [eventually_map, eventually_atTop, ge_iff_le, Set.mem_setOf_eq] at hb ⊢
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
b : ℝ
hb :
  ∃ (a : ℕ),
    ∀ (b_1 : ℕ),
      a ≤ b_1 →
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b_1)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤ b
⊢ ∃ (a : ℕ),
    ∀ (b_1 : ℕ),
      a ≤ b_1 → HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ b_1)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤ b
have obtain : ∀ (m : ℕ)
  (hm :
    ∀ (b_1 : ℕ),
      m ≤ b_1 →
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b_1)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤ b),
  ∃ (a : ℕ),
    ∀ (b_1 : ℕ),
      a ≤ b_1 → HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ b_1)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤ b
Tactic: obtain ⟨m, hm⟩ := hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
b : ℝ
m : ℕ
hm :
  ∀ (b_1 : ℕ),
    m ≤ b_1 →
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b_1)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤ b
⊢ ∃ (a : ℕ),
    ∀ (b_1 : ℕ),
      a ≤ b_1 → HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ b_1)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤ b
have h : ∀ (b_1 : ℕ),
  m ≤ b_1 → HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ b_1)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤ b
Tactic: use m
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
b : ℝ
m : ℕ
hm :
  ∀ (b_1 : ℕ),
    m ≤ b_1 →
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b_1)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤ b
k : ℕ
hkm : m ≤ k
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ k)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ k) : ℝ)) ≤ b
have apply : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ k)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ k) : ℝ)) ≤
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ k)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ k) : ℝ))
Tactic: apply le_trans _ (hm k hkm)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
b : ℝ
m : ℕ
hm :
  ∀ (b_1 : ℕ),
    m ≤ b_1 →
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b_1)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤ b
k : ℕ
hkm : m ≤ k
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ k)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ k) : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ k)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ k) : ℝ))
have rw : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ k)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ k) : ℝ)) ≤
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (s (ψ k)) ^ HDiv.hDiv (α := ℝ) 1 (↑(ψ k) : ℝ)
Tactic: rw [rpow_mul (apply_nonneg μ x), rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
b : ℝ
m : ℕ
hm :
  ∀ (b_1 : ℕ),
    m ≤ b_1 →
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b_1)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤ b
k : ℕ
hkm : m ≤ k
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ k)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ k) : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (s (ψ k)) ^ HDiv.hDiv (α := ℝ) 1 (↑(ψ k) : ℝ)
have h₁ : (μ : (a : R) → ℝ) (x ^ s (ψ k)) ≤ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (s (ψ k))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
⊢ BddBelow (α := ℝ)
    {a : ℝ |
      ∀ᶠ (n : ℝ) in
        map (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
          atTop,
        n ≤ a}
have h : Membership.mem (γ := Set ℝ)
  (lowerBounds
    {a : ℝ |
      ∀ᶠ (n : ℝ) in
        map (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
          atTop,
        n ≤ a})
  0
Tactic: use 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
⊢ Membership.mem (γ := Set ℝ)
    (lowerBounds
      {a : ℝ |
        ∀ᶠ (n : ℝ) in
          map
            (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
            atTop,
          n ≤ a})
    0
have h : ∀ (x_1 : ℝ) (x_2 : ℕ)
  (h :
    ∀ (b : ℕ),
      x_2 ≤ b → HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ b)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤ x_1),
  0 ≤ x_1
Tactic: simp only [mem_lowerBounds, eventually_map, eventually_atTop, ge_iff_le,
              Set.mem_setOf_eq, forall_exists_index]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
⊢ 1 = smoothingFun μ x ^ a
have rw : 1 = HPow.hPow (β := ℝ) (smoothingFun μ x) 0
Tactic: rw [ha, rpow_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
rw : 1 = HPow.hPow (β := ℝ) (smoothingFun μ x) 0
⊢ 1 = smoothingFun μ x ^ a
have rw₁ : Eq (α := ℝ) 1 1
Tactic: rw [ha, rpow_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
⊢ limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a
have calc : LE.le (α := ℝ)
  (limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
    atTop)
  (limsup
    (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
    atTop)
Tactic: calc limsup (fun n : ℕ => μ (x ^ s (ψ n)) ^ (1 / (ψ n : ℝ))) atTop ≤
          limsup (fun n : ℕ => μ x ^ ((s (ψ n) : ℝ) * (1 / (ψ n : ℝ)))) atTop := by
          apply csInf_le_csInf _ (μ_nonempty μ hs_le ψ)
          · intro b hb
            simp only [eventually_map, eventually_atTop, ge_iff_le, Set.mem_setOf_eq] at hb ⊢
            obtain ⟨m, hm⟩ := hb
            use m
            intro k hkm
            apply le_trans _ (hm k hkm)
            rw [rpow_mul (apply_nonneg μ x), rpow_natCast]
            gcongr
            exact map_pow_le_pow' hμ1 x _
          · use 0
            simp only [mem_lowerBounds, eventually_map, eventually_atTop, ge_iff_le,
              Set.mem_setOf_eq, forall_exists_index]
            exact fun _ m hm ↦ le_trans (by positivity) (hm m (le_refl _))
      _ ≤ 1 := (μ_limsup_le_one μ hs_le hψ_lim)
      _ = smoothingFun μ x ^ a := by rw [ha, rpow_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
calc :
  LE.le (α := ℝ)
    (limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop)
    (limsup
      (fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop)
⊢ limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a
have calc₁ : 1 = smoothingFun μ x ^ a
Tactic: calc limsup (fun n : ℕ => μ (x ^ s (ψ n)) ^ (1 / (ψ n : ℝ))) atTop ≤
          limsup (fun n : ℕ => μ x ^ ((s (ψ n) : ℝ) * (1 / (ψ n : ℝ)))) atTop := by
          apply csInf_le_csInf _ (μ_nonempty μ hs_le ψ)
          · intro b hb
            simp only [eventually_map, eventually_atTop, ge_iff_le, Set.mem_setOf_eq] at hb ⊢
            obtain ⟨m, hm⟩ := hb
            use m
            intro k hkm
            apply le_trans _ (hm k hkm)
            rw [rpow_mul (apply_nonneg μ x), rpow_natCast]
            gcongr
            exact map_pow_le_pow' hμ1 x _
          · use 0
            simp only [mem_lowerBounds, eventually_map, eventually_atTop, ge_iff_le,
              Set.mem_setOf_eq, forall_exists_index]
            exact fun _ m hm ↦ le_trans (by positivity) (hm m (le_refl _))
      _ ≤ 1 := (μ_limsup_le_one μ hs_le hψ_lim)
      _ = smoothingFun μ x ^ a := by rw [ha, rpow_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
⊢ limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a
have ha_pos : 0 < a
Tactic: have ha_pos : 0 < a := lt_of_le_of_ne a_in.1 (Ne.symm ha)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
⊢ EventuallyEq (β := ℝ) atTop (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑(s (ψ n)) : ℝ) * (↑(s (ψ n)) : ℝ)) 1
have hg : Tendsto (β := ℝ) (fun (x : ℕ) ↦ (↑(s (ψ x)) : ℝ)) atTop atTop
Tactic: apply Filter.EventuallyEq.div_mul_cancel_atTop
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
⊢ EventuallyEq (β := ℝ) atTop
    (fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(s (ψ n)) : ℝ)) ^
        HDiv.hDiv (α := ℝ) (↑(s (ψ n)) : ℝ) (↑(ψ n) : ℝ))
    fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))
have h : EventuallyEq (β := ℝ) atTop (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑(s (ψ n)) : ℝ) * (↑(s (ψ n)) : ℝ)) 1
Tactic: have h : (fun n : ℕ => (1 : ℝ) / (s (ψ n) : ℝ) * (s (ψ n) : ℝ)) =ᶠ[atTop] 1 := by
        apply Filter.EventuallyEq.div_mul_cancel_atTop
        exact (tendsto_natCast_atTop_atTop.comp hψ_mono.tendsto_atTop).num ha_pos hψ_lim
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
h : EventuallyEq (β := ℝ) atTop (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑(s (ψ n)) : ℝ) * (↑(s (ψ n)) : ℝ)) 1
⊢ EventuallyEq (β := ℝ) atTop
    (fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(s (ψ n)) : ℝ)) ^
        HDiv.hDiv (α := ℝ) (↑(s (ψ n)) : ℝ) (↑(ψ n) : ℝ))
    fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))
have simp_rw : EventuallyEq (β := ℝ) atTop
  (fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑(s (ψ n)) : ℝ) * (↑(s (ψ n)) : ℝ) / (↑(ψ n) : ℝ)))
  fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))
Tactic: simp_rw [← rpow_mul (apply_nonneg μ _), mul_div]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
⊢ limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a
have h_eq : EventuallyEq (β := ℝ) atTop
  (fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(s (ψ n)) : ℝ)) ^
      HDiv.hDiv (α := ℝ) (↑(s (ψ n)) : ℝ) (↑(ψ n) : ℝ))
  fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))
Tactic: have h_eq : (fun n : ℕ =>
        (μ (x ^ s (ψ n)) ^ (1 / (s (ψ n) : ℝ))) ^ ((s (ψ n) : ℝ) / (ψ n : ℝ))) =ᶠ[atTop]
        fun n : ℕ => μ (x ^ s (ψ n)) ^ (1 / (ψ n : ℝ)) := by
      have h : (fun n : ℕ => (1 : ℝ) / (s (ψ n) : ℝ) * (s (ψ n) : ℝ)) =ᶠ[atTop] 1 := by
        apply Filter.EventuallyEq.div_mul_cancel_atTop
        exact (tendsto_natCast_atTop_atTop.comp hψ_mono.tendsto_atTop).num ha_pos hψ_lim
      simp_rw [← rpow_mul (apply_nonneg μ _), mul_div]
      exact EventuallyEq.comp₂ EventuallyEq.rfl HPow.hPow (h.div EventuallyEq.rfl)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
x y : R
⊢ smoothingFun μ (x + y) ≤ max (smoothingFun μ x) (smoothingFun μ y)
have hn : ∀ (n : ℕ),
  ∃ m < n + 1,
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x + y) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
      HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ m) : ℝ) ((μ : (a : R) → ℝ) (y ^ (n - m)) : ℝ) ^
        HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
Tactic: have hn : ∀ n : ℕ, ∃ m < n + 1,
      μ ((x + y) ^ (n : ℕ)) ^ (1 / (n : ℝ)) ≤ (μ (x ^ m) * μ (y ^ (n - m : ℕ))) ^ (1 / (n : ℝ)) :=
    fun n => RingSeminorm.exists_index_pow_le μ hna x y n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
x y : R
hn :
  ∀ (n : ℕ),
    ∃ m < n + 1,
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x + y) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
        HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ m) : ℝ) ((μ : (a : R) → ℝ) (y ^ (n - m)) : ℝ) ^
          HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
mu : ℕ → ℕ := fun (n : ℕ) ↦ _root_.mu μ hn n
⊢ smoothingFun μ (x + y) ≤ max (smoothingFun μ x) (smoothingFun μ y)
have hnu : let nu : ℕ → ℕ := fun (n : ℕ) ↦ n - mu n;
nu = fun (n : ℕ) ↦ n - mu n
Tactic: set nu : ℕ → ℕ := fun n => n - mu n with hnu
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
x y : R
hn :
  ∀ (n : ℕ),
    ∃ m < n + 1,
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x + y) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
        HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ m) : ℝ) ((μ : (a : R) → ℝ) (y ^ (n - m)) : ℝ) ^
          HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
mu : ℕ → ℕ := fun (n : ℕ) ↦ _root_.mu μ hn n
nu : ℕ → ℕ := fun (n : ℕ) ↦ n - mu n
hnu : nu = fun (n : ℕ) ↦ n - mu n
⊢ smoothingFun μ (x + y) ≤ max (smoothingFun μ x) (smoothingFun μ y)
have hmu_le : ∀ (n : ℕ), mu n ≤ n
Tactic: have hmu_le : ∀ n : ℕ, mu n ≤ n := fun n => mu_le μ hn n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
x y : R
hn :
  ∀ (n : ℕ),
    ∃ m < n + 1,
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x + y) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
        HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ m) : ℝ) ((μ : (a : R) → ℝ) (y ^ (n - m)) : ℝ) ^
          HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
mu : ℕ → ℕ := fun (n : ℕ) ↦ _root_.mu μ hn n
nu : ℕ → ℕ := fun (n : ℕ) ↦ n - mu n
hnu : nu = fun (n : ℕ) ↦ n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
⊢ smoothingFun μ (x + y) ≤ max (smoothingFun μ x) (smoothingFun μ y)
have hmu_bdd : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ))
Tactic: have hmu_bdd : ∀ n : ℕ, (mu n : ℝ) / n ∈ Set.Icc (0 : ℝ) 1 := fun n => mu_bdd μ hn n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
x y : R
hn :
  ∀ (n : ℕ),
    ∃ m < n + 1,
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x + y) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
        HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ m) : ℝ) ((μ : (a : R) → ℝ) (y ^ (n - m)) : ℝ) ^
          HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
mu : ℕ → ℕ := fun (n : ℕ) ↦ _root_.mu μ hn n
nu : ℕ → ℕ := fun (n : ℕ) ↦ n - mu n
hnu : nu = fun (n : ℕ) ↦ n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ))
⊢ smoothingFun μ (x + y) ≤ max (smoothingFun μ x) (smoothingFun μ y)
have hs : Bornology.IsBounded (α := ℝ) (Set.Icc 0 1)
Tactic: have hs : Bornology.IsBounded (Set.Icc (0 : ℝ) 1) := Metric.isBounded_Icc 0 1