awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h_1 : Meromorphic f
h₁f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖) 0 r
θ : ℂ
hθ : Membership.mem (γ := Set ℂ) (sphere 0 |r|) θ
h : ¬0 ≤ log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖
h₁ : ‖f θ - a₀‖ = ‖-f θ + a₀‖
⊢ log⁺ ‖f θ - a₀‖ ≤ log⁺ ‖f θ‖ + log⁺ ‖a₀‖ + log 2
have h₂ : log⁺ ‖f θ‖ + log⁺ ‖a₀‖ = log⁺ ‖-f θ‖ + log⁺ ‖a₀‖
Tactic: convert! posLog_norm_add_le (-f θ) (a₀) using 2
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h_1 : Meromorphic f
h₁f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖) 0 r
θ : ℂ
hθ : Membership.mem (γ := Set ℂ) (sphere 0 |r|) θ
h : ¬0 ≤ log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖
⊢ ‖f θ - a₀‖ = ‖-f θ + a₀‖
have h₁ : ‖-(f θ - a₀)‖ = ‖-f θ + a₀‖
Tactic: rw [← norm_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
e : E
⊢ IsLittleO (α := ℝ) (E := ℝ) (F := ℝ) atTop 1 ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1))
have hΘ : IsTheta (E := ℝ) atTop (fun (r : ℝ) ↦ log r - log ‖e‖) log
Tactic: have hΘ : (fun r ↦ log r - log ‖e‖) =Θ[atTop] log :=
    (IsEquivalent.sub_isLittleO IsEquivalent.refl isLittleO_const_log_atTop).isTheta
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
e : E
hΘ : IsTheta (E := ℝ) atTop (fun (r : ℝ) ↦ log r - log ‖e‖) log
⊢ IsLittleO (α := ℝ) (E := ℝ) (F := ℝ) atTop 1 ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1))
have h₁ : IsLittleO (E := ℝ) (F := ℝ) atTop 1 fun (r : ℝ) ↦ log r - log ‖e‖
Tactic: have h₁ : (1 : ℝ → ℝ) =o[atTop] fun r ↦ log r - log ‖e‖ :=
    (hΘ.isLittleO_congr_right).2 isLittleO_const_log_atTop
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
e : E
hΘ : IsTheta (E := ℝ) atTop (fun (r : ℝ) ↦ log r - log ‖e‖) log
h₁ : IsLittleO (E := ℝ) (F := ℝ) atTop 1 fun (r : ℝ) ↦ log r - log ‖e‖
⊢ IsLittleO (α := ℝ) (E := ℝ) (F := ℝ) atTop 1 ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1))
have refine : EventuallyEq (β := ℝ) atTop (fun (r : ℝ) ↦ log r - log ‖e‖)
  ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1))
Tactic: refine h₁.congr' EventuallyEq.rfl ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
e : E
hΘ : IsTheta (E := ℝ) atTop (fun (r : ℝ) ↦ log r - log ‖e‖) log
h₁ : IsLittleO (E := ℝ) (F := ℝ) atTop 1 fun (r : ℝ) ↦ log r - log ‖e‖
⊢ EventuallyEq (β := ℝ) atTop (fun (r : ℝ) ↦ log r - log ‖e‖)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1))
have h : ∀ (r : ℝ) (hr : ‖e‖ ≤ r), log r - log ‖e‖ = (logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) r
Tactic: filter_upwards [eventually_ge_atTop ‖e‖] with r hr
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
⊢ D = 0 ↔ IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
have refine : IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1 → D = 0
Tactic: refine ⟨fun h₂ ↦ by simp [isBigO_of_le' (c := 0), h₂], ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
⊢ IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1 → D = 0
have contrapose : ¬D = 0 → ¬IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
⊢ ¬IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
have obtain : ∀ (e : E) (he : single e 1 ≤ D),
  ¬IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
Tactic: obtain ⟨e, he⟩ := exists_single_le_pos (lt_of_le_of_ne h (h₁ ·.symm))
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
⊢ ¬IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
have rw : ¬∃ c > 0,
    ∀ᶠ (x : ℝ) in atTop,
      c * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D x : ℝ) ≤ Norm.norm (E := ℝ) (1 x)
Tactic: rw [isBigO_iff'']
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
⊢ ¬∃ c > 0,
      ∀ᶠ (x : ℝ) in atTop,
        c * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D x : ℝ) ≤ Norm.norm (E := ℝ) (1 x)
have push : ∀ (c : ℝ) (_ : c > 0),
  ∃ᶠ (x : ℝ) in atTop,
    Norm.norm (E := ℝ) (1 x) < c * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D x : ℝ)
Tactic: push Not
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
⊢ ∃ᶠ (x : ℝ) in atTop,
    Norm.norm (E := ℝ) (1 x) < a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D x : ℝ)
have simp : ∀ (a_1 : ℝ), ∃ b ≥ a_1, 1 < HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D b| : ℝ)
Tactic: simp only [Pi.one_apply, norm_eq_abs, frequently_atTop, abs_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b : ℝ
⊢ ∃ b_1 ≥ b, 1 < HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D b_1| : ℝ)
have obtain : ∀ (c : ℝ)
  (hc :
    ∀ b ≥ c,
      Norm.norm (E := ℝ) (1 b) ≤
        a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)),
  ∃ b_1 ≥ b, 1 < HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D b_1| : ℝ)
Tactic: obtain ⟨c, hc⟩ := eventually_atTop.1
    (isLittleO_iff.1 (one_isLittleO_logCounting_single (e := e)) ha)
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
⊢ ∃ b_1 ≥ b, 1 < HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D b_1| : ℝ)
have h₁ℓ : c ≤ ℓ
Tactic: have h₁ℓ : c ≤ ℓ := by grind
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
⊢ ∃ b_1 ≥ b, 1 < HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D b_1| : ℝ)
have h₂ℓ : 1 ≤ ℓ
Tactic: have h₂ℓ : 1 ≤ ℓ := by simp [ℓ]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ ∃ b_1 ≥ b, 1 < HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D b_1| : ℝ)
have right : 1 < HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D (1 + ℓ)| : ℝ)
Tactic: use 1 + ℓ, (show b ≤ 1 + ℓ by grind)
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) ℓ| : ℝ) ≤
    HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D ℓ| : ℝ)
have hbc : LE.le (α := ℝ) (0 : ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) ℓ : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
hbc : LE.le (α := ℝ) (0 : ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) ℓ : ℝ)
⊢ HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) ℓ| : ℝ) ≤
    HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D ℓ| : ℝ)
have hbc₁ : LE.le (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) ℓ : ℝ)
  ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D ℓ : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D ℓ| : ℝ) <
    HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D (1 + ℓ)| : ℝ)
have hbc : LT.lt (α := ℝ) (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D ℓ| : ℝ)
  (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D (1 + ℓ)| : ℝ)
Tactic: gcongr 2
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ LT.lt (α := ℝ) (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D ℓ| : ℝ)
    (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D (1 + ℓ)| : ℝ)
have hbc : LT.lt (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D ℓ : ℝ)
  ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D (1 + ℓ) : ℝ)
Tactic: rw [abs_of_nonneg (logCounting_nonneg h h₂ℓ),
        abs_of_nonneg (logCounting_nonneg h (by grind))]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ LT.lt (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D ℓ : ℝ)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D (1 + ℓ) : ℝ)
have hbc : ℓ ∈ Ioi ‖e‖
Tactic: apply logCounting_strictMono he
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
hbc : ℓ ∈ Ioi ‖e‖
⊢ LT.lt (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D ℓ : ℝ)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D (1 + ℓ) : ℝ)
have hbc₁ : 1 + ℓ ∈ Ioi ‖e‖
Tactic: apply logCounting_strictMono he
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
hbc : ℓ ∈ Ioi ‖e‖
hbc₁ : 1 + ℓ ∈ Ioi ‖e‖
⊢ LT.lt (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D ℓ : ℝ)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D (1 + ℓ) : ℝ)
have hbc₂ : ℓ < 1 + ℓ
Tactic: apply logCounting_strictMono he
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ 1 < HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D (1 + ℓ)| : ℝ)
have calc : 1 ≤ HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) ℓ| : ℝ)
Tactic: calc 1
    _ ≤ (a * |logCounting (single e 1) ℓ|) := by simpa [h₁ℓ] using hc ℓ
    _ ≤ (a * |logCounting D ℓ|) := by
      gcongr
      · apply logCounting_nonneg (single_pos.2 Int.one_pos).le h₂ℓ
      · apply logCounting_le he h₂ℓ
    _ < a * |logCounting D (1 + ℓ)| := by
      gcongr 2
      rw [abs_of_nonneg (logCounting_nonneg h h₂ℓ),
        abs_of_nonneg (logCounting_nonneg h (by grind))]
      apply logCounting_strictMono he <;> grind
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
calc : 1 ≤ HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) ℓ| : ℝ)
⊢ 1 < HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D (1 + ℓ)| : ℝ)
have calc₁ : HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) ℓ| : ℝ) ≤
  HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D ℓ| : ℝ)
Tactic: calc 1
    _ ≤ (a * |logCounting (single e 1) ℓ|) := by simpa [h₁ℓ] using hc ℓ
    _ ≤ (a * |logCounting D ℓ|) := by
      gcongr
      · apply logCounting_nonneg (single_pos.2 Int.one_pos).le h₂ℓ
      · apply logCounting_le he h₂ℓ
    _ < a * |logCounting D (1 + ℓ)| := by
      gcongr 2
      rw [abs_of_nonneg (logCounting_nonneg h h₂ℓ),
        abs_of_nonneg (logCounting_nonneg h (by grind))]
      apply logCounting_strictMono he <;> grind
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
calc : 1 ≤ HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) ℓ| : ℝ)
calc₁ :
  HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) ℓ| : ℝ) ≤
    HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D ℓ| : ℝ)
⊢ 1 < HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D (1 + ℓ)| : ℝ)
have calc₂ : HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D ℓ| : ℝ) <
  HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D (1 + ℓ)| : ℝ)
Tactic: calc 1
    _ ≤ (a * |logCounting (single e 1) ℓ|) := by simpa [h₁ℓ] using hc ℓ
    _ ≤ (a * |logCounting D ℓ|) := by
      gcongr
      · apply logCounting_nonneg (single_pos.2 Int.one_pos).le h₂ℓ
      · apply logCounting_le he h₂ℓ
    _ < a * |logCounting D (1 + ℓ)| := by
      gcongr 2
      rw [abs_of_nonneg (logCounting_nonneg h h₂ℓ),
        abs_of_nonneg (logCounting_nonneg h (by grind))]
      apply logCounting_strictMono he <;> grind
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
⊢ D = 0 ↔ IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
have refine : IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1 → D = 0
Tactic: classical
  refine ⟨fun h₂ ↦ by simp [isBigO_of_le' (c := 0), h₂], ?_⟩
  contrapose
  intro h₁
  obtain ⟨e, he⟩ := exists_single_le_pos (lt_of_le_of_ne h (h₁ ·.symm))
  rw [isBigO_iff'']
  push Not
  intro a ha
  simp only [Pi.one_apply, norm_eq_abs, frequently_atTop, abs_one]
  intro b
  obtain ⟨c, hc⟩ := eventually_atTop.1
    (isLittleO_iff.1 (one_isLittleO_logCounting_single (e := e)) ha)
  let ℓ := 1 + max ‖e‖ (max |b| |c|)
  have h₁ℓ : c ≤ ℓ := by grind
  have h₂ℓ : 1 ≤ ℓ := by simp [ℓ]
  use 1 + ℓ, (show b ≤ 1 + ℓ by grind)
  calc 1
    _ ≤ (a * |logCounting (single e 1) ℓ|) := by simpa [h₁ℓ] using hc ℓ
    _ ≤ (a * |logCounting D ℓ|) := by
      gcongr
      · apply logCounting_nonneg (single_pos.2 Int.one_pos).le h₂ℓ
      · apply logCounting_le he h₂ℓ
    _ < a * |logCounting D (1 + ℓ)| := by
      gcongr 2
      rw [abs_of_nonneg (logCounting_nonneg h h₂ℓ),
        abs_of_nonneg (logCounting_nonneg h (by grind))]
      apply logCounting_strictMono he <;> grind
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
refine : IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1 → D = 0
⊢ D = 0 ↔ IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
have refine₁ : ¬D = 0 → ¬IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
Tactic: classical
  refine ⟨fun h₂ ↦ by simp [isBigO_of_le' (c := 0), h₂], ?_⟩
  contrapose
  intro h₁
  obtain ⟨e, he⟩ := exists_single_le_pos (lt_of_le_of_ne h (h₁ ·.symm))
  rw [isBigO_iff'']
  push Not
  intro a ha
  simp only [Pi.one_apply, norm_eq_abs, frequently_atTop, abs_one]
  intro b
  obtain ⟨c, hc⟩ := eventually_atTop.1
    (isLittleO_iff.1 (one_isLittleO_logCounting_single (e := e)) ha)
  let ℓ := 1 + max ‖e‖ (max |b| |c|)
  have h₁ℓ : c ≤ ℓ := by grind
  have h₂ℓ : 1 ≤ ℓ := by simp [ℓ]
  use 1 + ℓ, (show b ≤ 1 + ℓ by grind)
  calc 1
    _ ≤ (a * |logCounting (single e 1) ℓ|) := by simpa [h₁ℓ] using hc ℓ
    _ ≤ (a * |logCounting D ℓ|) := by
      gcongr
      · apply logCounting_nonneg (single_pos.2 Int.one_pos).le h₂ℓ
      · apply logCounting_le he h₂ℓ
    _ < a * |logCounting D (1 + ℓ)| := by
      gcongr 2
      rw [abs_of_nonneg (logCounting_nonneg h h₂ℓ),
        abs_of_nonneg (logCounting_nonneg h (by grind))]
      apply logCounting_strictMono he <;> grind
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
refine : IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1 → D = 0
refine₁ refine₂ :
  ∀ (h₁ : ¬D = 0), ¬IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
⊢ D = 0 ↔ IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
have refine₃ : ∀ (h₁ : ¬D = 0) (e : E) (he : single e 1 ≤ D),
  ¬IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
Tactic: classical
  refine ⟨fun h₂ ↦ by simp [isBigO_of_le' (c := 0), h₂], ?_⟩
  contrapose
  intro h₁
  obtain ⟨e, he⟩ := exists_single_le_pos (lt_of_le_of_ne h (h₁ ·.symm))
  rw [isBigO_iff'']
  push Not
  intro a ha
  simp only [Pi.one_apply, norm_eq_abs, frequently_atTop, abs_one]
  intro b
  obtain ⟨c, hc⟩ := eventually_atTop.1
    (isLittleO_iff.1 (one_isLittleO_logCounting_single (e := e)) ha)
  let ℓ := 1 + max ‖e‖ (max |b| |c|)
  have h₁ℓ : c ≤ ℓ := by grind
  have h₂ℓ : 1 ≤ ℓ := by simp [ℓ]
  use 1 + ℓ, (show b ≤ 1 + ℓ by grind)
  calc 1
    _ ≤ (a * |logCounting (single e 1) ℓ|) := by simpa [h₁ℓ] using hc ℓ
    _ ≤ (a * |logCounting D ℓ|) := by
      gcongr
      · apply logCounting_nonneg (single_pos.2 Int.one_pos).le h₂ℓ
      · apply logCounting_le he h₂ℓ
    _ < a * |logCounting D (1 + ℓ)| := by
      gcongr 2
      rw [abs_of_nonneg (logCounting_nonneg h h₂ℓ),
        abs_of_nonneg (logCounting_nonneg h (by grind))]
      apply logCounting_strictMono he <;> grind