awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℝ))
hs : Bornology.IsBounded (α := ℝ) (Set.Icc 0 1)
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(nu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 b)
b_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) b
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a
hy :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ y ^ b
⊢ limsup
      (fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
have hxy' : limsup
    (fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) *
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
    atTop ≤
  HMul.hMul (α := ℝ)
    (limsup
      (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop)
    (limsup
      (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop)
Tactic: have hxy' :
      limsup (fun n : ℕ => μ (x ^ mu (ψ n)) ^ (1 / (ψ n : ℝ)) * μ (y ^ nu (ψ n)) ^ (1 / (ψ n : ℝ)))
        atTop ≤ limsup (fun n : ℕ => μ (x ^ mu (ψ n)) ^ (1 / (ψ n : ℝ))) atTop *
          limsup (fun n : ℕ => μ (y ^ nu (ψ n)) ^ (1 / (ψ n : ℝ))) atTop :=
      limsup_mul_le (Frequently.of_forall (fun n ↦ by positivity))
        (μ_bddAbove μ hμ1 hmu_le x ψ).isBoundedUnder_of_range
        (Eventually.of_forall (fun n ↦ by positivity))
        (μ_bddAbove μ hμ1 hnu_le y ψ).isBoundedUnder_of_range
-- 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 : ℝ))
hs : Bornology.IsBounded (α := ℝ) (Set.Icc 0 1)
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(nu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 b)
b_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) b
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a
hy :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ y ^ b
hxy' :
  limsup
      (fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    HMul.hMul (α := ℝ)
      (limsup
        (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
        atTop)
      (limsup
        (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
        atTop)
⊢ limsup
      (fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
have h_bdd : IsBoundedUnder (α := ℝ) LE.le atTop fun (n : ℕ) ↦
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))
Tactic: have h_bdd : IsBoundedUnder LE.le atTop fun n : ℕ => μ (y ^ nu (ψ n)) ^ (1 / (ψ n : ℝ)) :=
      RingSeminorm.isBoundedUnder μ hμ1 hnu_le ψ
-- 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 : ℝ))
hs : Bornology.IsBounded (α := ℝ) (Set.Icc 0 1)
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(nu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 b)
b_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) b
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a
hy :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ y ^ b
⊢ smoothingFun μ (x + y) ≤ max (smoothingFun μ x) (smoothingFun μ y)
have hxy : limsup
    (fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) *
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
    atTop ≤
  smoothingFun μ x ^ a * smoothingFun μ y ^ b
Tactic: have hxy : limsup
      (fun n => μ (x ^ mu (ψ n)) ^ (1 / (ψ n : ℝ)) * μ (y ^ nu (ψ n)) ^ (1 / (ψ n : ℝ))) atTop ≤
        smoothingFun μ x ^ a * smoothingFun μ y ^ b := by
    have hxy' :
      limsup (fun n : ℕ => μ (x ^ mu (ψ n)) ^ (1 / (ψ n : ℝ)) * μ (y ^ nu (ψ n)) ^ (1 / (ψ n : ℝ)))
        atTop ≤ limsup (fun n : ℕ => μ (x ^ mu (ψ n)) ^ (1 / (ψ n : ℝ))) atTop *
          limsup (fun n : ℕ => μ (y ^ nu (ψ n)) ^ (1 / (ψ n : ℝ))) atTop :=
      limsup_mul_le (Frequently.of_forall (fun n ↦ by positivity))
        (μ_bddAbove μ hμ1 hmu_le x ψ).isBoundedUnder_of_range
        (Eventually.of_forall (fun n ↦ by positivity))
        (μ_bddAbove μ hμ1 hnu_le y ψ).isBoundedUnder_of_range
    have h_bdd : IsBoundedUnder LE.le atTop fun n : ℕ => μ (y ^ nu (ψ n)) ^ (1 / (ψ n : ℝ)) :=
      RingSeminorm.isBoundedUnder μ hμ1 hnu_le ψ
    apply le_trans hxy' (mul_le_mul hx hy (le_limsup_of_frequently_le (Frequently.of_forall
      (fun n ↦ by positivity)) h_bdd) (rpow_nonneg (smoothingFun_nonneg μ hμ1 x) _))
-- 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 : ℝ)
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 : ℝ))
hs : Bornology.IsBounded (α := ℝ) (Set.Icc 0 1)
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(nu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 b)
b_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) b
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a
hy :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ y ^ b
hxy :
  limsup
      (fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
⊢ smoothingFun μ (x + y) ≤ max (smoothingFun μ x) (smoothingFun μ y)
have h : ∀ ε > 0, smoothingFun μ (x + y) - ε ≤ max (smoothingFun μ x) (smoothingFun μ y)
Tactic: apply le_of_forall_sub_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 : ℝ)
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 : ℝ))
hs : Bornology.IsBounded (α := ℝ) (Set.Icc 0 1)
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(nu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 b)
b_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) b
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a
hy :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ y ^ b
hxy :
  limsup
      (fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
ε : ℝ
hε : ε > 0
⊢ smoothingFun μ (x + y) - ε ≤ max (smoothingFun μ x) (smoothingFun μ y)
have h : smoothingFun μ (x + y) ≤ max (smoothingFun μ x) (smoothingFun μ y) + ε
Tactic: rw [sub_le_iff_le_add]
-- 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 : ℝ)
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 : ℝ))
hs : Bornology.IsBounded (α := ℝ) (Set.Icc 0 1)
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(nu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 b)
b_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) b
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a
hy :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ y ^ b
hxy :
  limsup
      (fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
ε : ℝ
hε : ε > 0
⊢ smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤ max (smoothingFun μ x) (smoothingFun μ y) + ε
have rw : smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤
  (if smoothingFun μ x ≤ smoothingFun μ y then smoothingFun μ y else smoothingFun μ x) + ε
Tactic: rw [max_def]
-- 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 : ℝ)
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 : ℝ))
hs : Bornology.IsBounded (α := ℝ) (Set.Icc 0 1)
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(nu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 b)
b_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) b
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a
hy :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ y ^ b
hxy :
  limsup
      (fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
ε : ℝ
hε : ε > 0
⊢ smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤
    (if smoothingFun μ x ≤ smoothingFun μ y then smoothingFun μ y else smoothingFun μ x) + ε
have pos : ∀ (h : smoothingFun μ x ≤ smoothingFun μ y), smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤ smoothingFun μ y + ε
Tactic: split_ifs with h
-- 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 : ℝ)
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 : ℝ))
hs : Bornology.IsBounded (α := ℝ) (Set.Icc 0 1)
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(nu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 b)
b_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) b
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a
hy :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ y ^ b
hxy :
  limsup
      (fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
ε : ℝ
hε : ε > 0
pos :
  ∀ (h : smoothingFun μ x ≤ smoothingFun μ y), smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤ smoothingFun μ y + ε
⊢ smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤
    (if smoothingFun μ x ≤ smoothingFun μ y then smoothingFun μ y else smoothingFun μ x) + ε
have neg : ∀ (h : ¬smoothingFun μ x ≤ smoothingFun μ y), smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤ smoothingFun μ x + ε
Tactic: split_ifs with h
-- 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 : ℝ)
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 : ℝ))
hs : Bornology.IsBounded (α := ℝ) (Set.Icc 0 1)
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(nu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 b)
b_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) b
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a
hy :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ y ^ b
hxy :
  limsup
      (fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
ε : ℝ
hε : ε > 0
h : smoothingFun μ x ≤ smoothingFun μ y
⊢ smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤ smoothingFun μ y + ε
have pos : smoothingFun μ x ^ a * smoothingFun μ y ^ b ≤ smoothingFun μ y
Tactic: rw [add_le_add_iff_right]
-- 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 : ℝ)
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 : ℝ))
hs : Bornology.IsBounded (α := ℝ) (Set.Icc 0 1)
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(nu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 b)
b_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) b
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a
hy :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ y ^ b
hxy :
  limsup
      (fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
ε : ℝ
hε : ε > 0
h : smoothingFun μ x ≤ smoothingFun μ y
⊢ smoothingFun μ x ^ a * smoothingFun μ y ^ b ≤ smoothingFun μ y
have pos : smoothingFun μ y ^ a * smoothingFun μ y ^ b ≤ smoothingFun μ y
Tactic: apply le_trans (mul_le_mul_of_nonneg_right
        (rpow_le_rpow (smoothingFun_nonneg μ hμ1 _) h a_in.1)
        (rpow_nonneg (smoothingFun_nonneg μ hμ1 _) _))