awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a b : ℝ
ha : 0 < a
hb : 0 < b
h : a ≤ b
s : Set E :=
  support (U := closedBall 0 |b|) (Y := ℤ)
    ((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D)
hs : s.Finite
z : E
⊢ Membership.mem (γ := Set E)
      (Function.support (M := ℝ) fun (z : E) ↦
        (↑((((toClosedBall a : (a_1 : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |a|) ℤ) D :
                    locallyFinsuppWithin (X := E) (closedBall 0 |a|) ℤ) :
                  (a : E) → ℤ)
                z) :
            ℝ) *
          log (a * ‖z‖⁻¹))
      z →
    z ∈ (↑(hs.toFinset (s := s)) : Set E)
have h₁ : ¬Eq (α := ℤ)
      ((((toClosedBall a : (a_1 : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |a|) ℤ) D :
              locallyFinsuppWithin (X := E) (closedBall 0 |a|) ℤ) :
            (a : E) → ℤ)
          z :
        ℤ)
      (0 : ℤ) →
  ¬a = 0 →
    ¬z = 0 →
      ¬a * ‖z‖⁻¹ = 1 →
        ¬a * ‖z‖⁻¹ = -1 →
          ¬Eq (α := ℤ)
              ((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
                      locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
                    (a : E) → ℤ)
                  z :
                ℤ)
              (0 : ℤ)
Tactic: simp only [support_mul, mem_inter_iff, mem_support, ne_eq, Int.cast_eq_zero, log_eq_zero,
        mul_eq_zero, inv_eq_zero, norm_eq_zero, not_or, Finite.coe_toFinset, and_imp, s]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a b : ℝ
ha : 0 < a
hb : 0 < b
h : a ≤ b
s : Set E :=
  support (U := closedBall 0 |b|) (Y := ℤ)
    ((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D)
hs : s.Finite
z : E
h₁ :
  ¬Eq (α := ℤ)
      ((((toClosedBall a : (a_1 : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |a|) ℤ) D :
              locallyFinsuppWithin (X := E) (closedBall 0 |a|) ℤ) :
            (a : E) → ℤ)
          z :
        ℤ)
      (0 : ℤ)
h_1 : ¬a = 0
h_2 : ¬z = 0
h_3 : ¬a * ‖z‖⁻¹ = 1
h_4 : ¬a * ‖z‖⁻¹ = -1
⊢ ¬Eq (α := ℤ)
      ((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
              locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
            (a : E) → ℤ)
          z :
        ℤ)
      (0 : ℤ)
have this : Membership.mem (γ := Set E) (closedBall 0 |a|) z
Tactic: have : z ∈ closedBall 0 |a| := mem_of_indicator_ne_zero h₁
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a b : ℝ
ha : 0 < a
hb : 0 < b
h : a ≤ b
s : Set E :=
  support (U := closedBall 0 |b|) (Y := ℤ)
    ((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D)
hs : s.Finite
z : E
h₁ :
  ¬Eq (α := ℤ)
      ((((toClosedBall a : (a_1 : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |a|) ℤ) D :
              locallyFinsuppWithin (X := E) (closedBall 0 |a|) ℤ) :
            (a : E) → ℤ)
          z :
        ℤ)
      (0 : ℤ)
h_1 : ¬a = 0
h_2 : ¬z = 0
h_3 : ¬a * ‖z‖⁻¹ = 1
h_4 : ¬a * ‖z‖⁻¹ = -1
this : Membership.mem (γ := Set E) (closedBall 0 |a|) z
⊢ ¬Eq (α := ℤ)
      ((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
              locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
            (a : E) → ℤ)
          z :
        ℤ)
      (0 : ℤ)
have h₂ : ¬Eq (α := ℤ) ((D : (a : E) → ℤ) z : ℤ) (0 : ℤ)
Tactic: rw [toClosedBall_eval_within _ this] at h₁
Cleared hypotheses: h₁, h_1, h_2, h_3, h_4, this
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a b : ℝ
ha : 0 < a
hb : 0 < b
h : a ≤ b
s : Set E :=
  support (U := closedBall 0 |b|) (Y := ℤ)
    ((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D)
hs : s.Finite
z : E
h₁ : ¬Eq (α := ℤ) ((D : (a : E) → ℤ) z : ℤ) (0 : ℤ)
h_1 : ¬a = 0
h_2 : ¬z = 0
h_3 : ¬a * ‖z‖⁻¹ = 1
h_4 : ¬a * ‖z‖⁻¹ = -1
this : Membership.mem (γ := Set E) (closedBall 0 |a|) z
⊢ ¬Eq (α := ℤ)
      ((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
              locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
            (a : E) → ℤ)
          z :
        ℤ)
      (0 : ℤ)
have h₂ : Membership.mem (γ := Set E) (closedBall 0 |b|) z
Tactic: rwa [toClosedBall_eval_within]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a b : ℝ
ha : 0 < a
hb : 0 < b
h : a ≤ b
s : Set E :=
  support (U := closedBall 0 |b|) (Y := ℤ)
    ((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D)
hs : s.Finite
z : E
h₁ : ¬Eq (α := ℤ) ((D : (a : E) → ℤ) z : ℤ) (0 : ℤ)
h_1 : ¬a = 0
h_2 : ¬z = 0
h_3 : ¬a * ‖z‖⁻¹ = 1
h_4 : ¬a * ‖z‖⁻¹ = -1
this : Membership.mem (γ := Set E) (closedBall 0 |a|) z
⊢ Membership.mem (γ := Set E) (closedBall 0 |b|) z
have h₂ : ∀ (this : ‖z‖ ≤ a), ‖z‖ ≤ b
Tactic: simp_all only [abs_of_pos ha, mem_closedBall, dist_zero_right, abs_of_pos hb]
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a b : ℝ
ha : 0 < a
hb : 0 < b
h : a ≤ b
s : Set E :=
  support (U := closedBall 0 |b|) (Y := ℤ)
    ((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D)
hs : s.Finite
z : E
h₁ : ¬Eq (α := ℤ) ((D : (a : E) → ℤ) z : ℤ) (0 : ℤ)
h_1 : ¬a = 0
h_2 : ¬z = 0
h_3 : ¬a * ‖z‖⁻¹ = 1
h_4 : ¬a * ‖z‖⁻¹ = -1
this : ‖z‖ ≤ a
⊢ ‖z‖ ≤ b
have linarith : b < ‖z‖ → a - b + (‖z‖ - a) + (b - ‖z‖) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
⊢ StrictMonoOn (β := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) (Ioi ‖e‖)
have rw : StrictMonoOn
  (HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) : ℝ → ℝ)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (D - single e 1) : ℝ → ℝ))
  (Ioi ‖e‖)
Tactic: rw [(by aesop : logCounting D = logCounting (single e 1) + logCounting (D - single e 1))]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
⊢ StrictMonoOn
    (HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) : ℝ → ℝ)
      ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (D - single e 1) : ℝ → ℝ))
    (Ioi ‖e‖)
have hf : StrictMonoOn (β := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1)) (Ioi ‖e‖)
Tactic: apply StrictMonoOn.add_monotone
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
hf : StrictMonoOn (β := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1)) (Ioi ‖e‖)
⊢ StrictMonoOn
    (HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) : ℝ → ℝ)
      ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (D - single e 1) : ℝ → ℝ))
    (Ioi ‖e‖)
have hg : MonotoneOn (β := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (D - single e 1)) (Ioi ‖e‖)
Tactic: apply StrictMonoOn.add_monotone
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
a : ℝ
ha : a ∈ Ioi ‖e‖
b : ℝ
hb : b ∈ Ioi ‖e‖
hab : a < b
⊢ LT.lt (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) a : ℝ)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
have hf : ∀ (ha : ‖e‖ < a) ⦃b : ℝ⦄ (hb : ‖e‖ < b) (hab : a < b),
  LT.lt (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) a : ℝ)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
Tactic: rw [mem_Ioi] at ha hb
Cleared hypotheses: ha, b, hb, hab
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
a : ℝ
ha : ‖e‖ < a
b : ℝ
hb : ‖e‖ < b
hab : a < b
⊢ LT.lt (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) a : ℝ)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
have hf : (↑1 : ℝ) * (log a - log ‖e‖) < (↑1 : ℝ) * (log b - log ‖e‖)
Tactic: rw [logCounting_single_eq_log_sub_const ha.le, logCounting_single_eq_log_sub_const hb.le]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
a : ℝ
ha : ‖e‖ < a
b : ℝ
hb : ‖e‖ < b
hab : a < b
⊢ (↑1 : ℝ) * (log a - log ‖e‖) < (↑1 : ℝ) * (log b - log ‖e‖)
have hf : 0 < a
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
a : ℝ
ha : a ∈ Ioi ‖e‖
b : ℝ
hb : b ∈ Ioi ‖e‖
hab : a ≤ b
⊢ LE.le (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (D - single e 1) a : ℝ)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (D - single e 1) b : ℝ)
have apply : 0 ≤ D - single e 1
Tactic: apply logCounting_mono _ _ ((norm_nonneg e).trans_lt hb) hab
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
a : ℝ
ha : a ∈ Ioi ‖e‖
b : ℝ
hb : b ∈ Ioi ‖e‖
hab : a ≤ b
apply : 0 ≤ D - single e 1
⊢ LE.le (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (D - single e 1) a : ℝ)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (D - single e 1) b : ℝ)
have apply₁ : Membership.mem (γ := Set ℝ) (Ioi 0) a
Tactic: apply logCounting_mono _ _ ((norm_nonneg e).trans_lt hb) hab
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
f : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f
hr : 1 ≤ r
⊢ 0 < r
have linarith : r ≤ 0 → -1 + (1 - r) + (r - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
f : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f
hr : 1 ≤ r
⊢ LE.le (α := ℝ) (0 : ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f r : ℝ)
have h₃r : 0 < r
Tactic: have h₃r : 0 < r := by linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
f : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f
hr : 1 ≤ r
h₃r : 0 < r
⊢ LE.le (α := ℝ) (0 : ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f r : ℝ)
have suffices : ∀ (z : E),
  0 ≤
    (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) f :
                locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
              (a : E) → ℤ)
            z) :
        ℝ) *
      log (r * ‖z‖⁻¹)
Tactic: suffices ∀ z, 0 ≤ toClosedBall r f z * log (r * ‖z‖⁻¹) from
    add_nonneg (finsum_nonneg this) <| mul_nonneg (by simpa using h 0) (log_nonneg hr)
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
f : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f
hr : 1 ≤ r
h₃r : 0 < r
a : E
⊢ 0 ≤
    (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) f :
                locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
              (a : E) → ℤ)
            a) :
        ℝ) *
      log (r * ‖a‖⁻¹)
have pos : ∀ (h₁a : a = 0),
  0 ≤
    (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) f :
                locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
              (a : E) → ℤ)
            a) :
        ℝ) *
      log (r * ‖a‖⁻¹)
Tactic: by_cases h₁a : a = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
f : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f
hr : 1 ≤ r
h₃r : 0 < r
a : E
pos :
  ∀ (h₁a : a = 0),
    0 ≤
      (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) f :
                  locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                (a : E) → ℤ)
              a) :
          ℝ) *
        log (r * ‖a‖⁻¹)
⊢ 0 ≤
    (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) f :
                locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
              (a : E) → ℤ)
            a) :
        ℝ) *
      log (r * ‖a‖⁻¹)
have neg : ∀ (h₁a : ¬a = 0),
  0 ≤
    (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) f :
                locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
              (a : E) → ℤ)
            a) :
        ℝ) *
      log (r * ‖a‖⁻¹)
Tactic: by_cases h₁a : a = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
f : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f
hr : 1 ≤ r
h₃r : 0 < r
a : E
h₁a : ¬a = 0
⊢ 0 ≤
    (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) f :
                locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
              (a : E) → ℤ)
            a) :
        ℝ) *
      log (r * ‖a‖⁻¹)
have pos : ∀ (h₂a : Membership.mem (γ := Set E) (closedBall 0 |r|) a),
  0 ≤
    (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) f :
                locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
              (a : E) → ℤ)
            a) :
        ℝ) *
      log (r * ‖a‖⁻¹)
Tactic: by_cases h₂a : a ∈ closedBall 0 |r|
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
f : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f
hr : 1 ≤ r
h₃r : 0 < r
a : E
h₁a : ¬a = 0
pos :
  ∀ (h₂a : Membership.mem (γ := Set E) (closedBall 0 |r|) a),
    0 ≤
      (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) f :
                  locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                (a : E) → ℤ)
              a) :
          ℝ) *
        log (r * ‖a‖⁻¹)
⊢ 0 ≤
    (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) f :
                locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
              (a : E) → ℤ)
            a) :
        ℝ) *
      log (r * ‖a‖⁻¹)
have neg : ∀ (h₂a : a ∉ closedBall 0 |r|),
  0 ≤
    (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) f :
                locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
              (a : E) → ℤ)
            a) :
        ℝ) *
      log (r * ‖a‖⁻¹)
Tactic: by_cases h₂a : a ∈ closedBall 0 |r|
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
f : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f
hr : 1 ≤ r
h₃r : 0 < r
a : E
h₁a : ¬a = 0
h₂a : Membership.mem (γ := Set E) (closedBall 0 |r|) a
⊢ 0 ≤
    (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) f :
                locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
              (a : E) → ℤ)
            a) :
        ℝ) *
      log (r * ‖a‖⁻¹)
have pos : LE.le (α := ℝ) 0
  (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) f :
            locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
          (a : E) → ℤ)
        a) :
    ℝ)
Tactic: refine mul_nonneg ?_ <| log_nonneg ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
f : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f
hr : 1 ≤ r
h₃r : 0 < r
a : E
h₁a : ¬a = 0
h₂a : Membership.mem (γ := Set E) (closedBall 0 |r|) a
pos :
  LE.le (α := ℝ) 0
    (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) f :
              locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
            (a : E) → ℤ)
          a) :
      ℝ)
⊢ 0 ≤
    (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) f :
                locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
              (a : E) → ℤ)
            a) :
        ℝ) *
      log (r * ‖a‖⁻¹)
have pos₁ : 1 ≤ r * ‖a‖⁻¹
Tactic: refine mul_nonneg ?_ <| log_nonneg ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
f₁ f₂ : locallyFinsupp E ℤ
r : ℝ
h : f₁ ≤ f₂
hr : 1 ≤ r
⊢ LE.le (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₁ r : ℝ)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₂ r : ℝ)
have rw : ∀ (h : 0 ≤ f₂ - f₁) (hr : 1 ≤ r),
  0 ≤
    HSub.hSub (α := ℝ) (β := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₂ r : ℝ)
      ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₁ r : ℝ)
Tactic: rw [← sub_nonneg] at h ⊢
Cleared hypotheses: h, hr
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
f₁ f₂ : locallyFinsupp E ℤ
h : f₁ ≤ f₂
⊢ EventuallyLE (α := ℝ) (β := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₁)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₂)
have h₁ : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 1 ≤ x) x} x →
        Membership.mem (γ := Set ℝ)
          {x : ℝ |
            (fun (x : ℝ) ↦
                LE.le (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₁ x : ℝ)
                  ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₂ x : ℝ))
              x}
          x}
    a
Tactic: filter_upwards [eventually_ge_atTop 1] using fun _ hr ↦ logCounting_le h hr
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
f₁ f₂ : locallyFinsupp E ℤ
h : f₁ ≤ f₂
h₁ :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 1 ≤ x) x} x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ |
              (fun (x : ℝ) ↦
                  LE.le (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₁ x : ℝ)
                    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₂ x : ℝ))
                x}
            x}
      a
⊢ EventuallyLE (α := ℝ) (β := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₁)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₂)
have h₂ : ∀ (a : ℝ),
  1 ≤ a →
    LE.le (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₁ a : ℝ)
      ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₂ a : ℝ)
Tactic: filter_upwards [eventually_ge_atTop 1] using fun _ hr ↦ logCounting_le h hr
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
a : WithTop E
a₀ : E
⊢ ℝ → ℝ
have pos : (h : a = ⊤) → ℝ → ℝ
Tactic: by_cases h : a = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
a : WithTop E
a₀ : E
pos : (h : a = ⊤) → ℝ → ℝ
⊢ ℝ → ℝ
have neg : (h : ¬a = ⊤) → ℝ → ℝ
Tactic: by_cases h : a = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : 𝕜 → E
a : WithTop E
⊢ logCounting f a 0 = 0
have pos : ∀ (h : a = ⊤), logCounting f a 0 = 0
Tactic: by_cases h : a = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : 𝕜 → E
a : WithTop E
pos : ∀ (h : a = ⊤), logCounting f a 0 = 0
⊢ logCounting f a 0 = 0
have neg : ∀ (h : ¬a = ⊤), logCounting f a 0 = 0
Tactic: by_cases h : a = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : 𝕜 → E
⊢ (locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor f univ) =
    logCounting f 0 - logCounting f ⊤
have rw : (locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
    (HSub.hSub (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (divisor f univ)⁺ (divisor f univ)⁻) =
  logCounting f 0 - logCounting f ⊤
Tactic: rw [← posPart_sub_negPart (divisor f univ), logCounting_zero, logCounting_top, map_sub]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : 𝕜 → E
rw :
  (locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
      (HSub.hSub (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (divisor f univ)⁺ (divisor f univ)⁻) =
    logCounting f 0 - logCounting f ⊤
⊢ (locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor f univ) =
    logCounting f 0 - logCounting f ⊤
have rw₁ : (locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
    (HSub.hSub (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (divisor f univ)⁺ (divisor f univ)⁻) =
  HSub.hSub (α := ℝ → ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor f univ)⁺ : ℝ → ℝ) (logCounting f ⊤)
Tactic: rw [← posPart_sub_negPart (divisor f univ), logCounting_zero, logCounting_top, map_sub]