awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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₂ :
  ¬a * ‖z‖⁻¹ = -1 →
    ¬Eq (α := ℤ)
        ((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
                locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
              (a : E) → ℤ)
            z :
          ℤ)
        (0 : ℤ)
⊢ ¬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:
_
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
⊢ Membership.mem (γ := Set E) (closedBall 0 |a|) z

Tactic:
have : z ∈ closedBall 0 |a| := mem_of_indicator_ne_zero h₁
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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 (α := ℤ) ((D : (a : E) → ℤ) z : ℤ) (0 : ℤ)

Tactic:
rw [toClosedBall_eval_within _ this] at h₁

Premises used: Function.locallyFinsuppWithin.toClosedBall_eval_within
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
h₂ : ¬Eq (α := ℤ) ((D : (a : E) → ℤ) z : ℤ) (0 : ℤ)
⊢ ¬a = 0

Tactic:
rw [toClosedBall_eval_within _ this] at h₁

Premises used: Function.locallyFinsuppWithin.toClosedBall_eval_within
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
h₂ : ¬Eq (α := ℤ) ((D : (a : E) → ℤ) z : ℤ) (0 : ℤ)
a₁ : ¬a = 0
⊢ ¬z = 0

Tactic:
rw [toClosedBall_eval_within _ this] at h₁

Premises used: Function.locallyFinsuppWithin.toClosedBall_eval_within
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
h₂ : ¬Eq (α := ℤ) ((D : (a : E) → ℤ) z : ℤ) (0 : ℤ)
a₁ : ¬a = 0
a₂ : ¬z = 0
⊢ ¬a * ‖z‖⁻¹ = 1

Tactic:
rw [toClosedBall_eval_within _ this] at h₁

Premises used: Function.locallyFinsuppWithin.toClosedBall_eval_within
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
h₂ : ¬Eq (α := ℤ) ((D : (a : E) → ℤ) z : ℤ) (0 : ℤ)
a₁ : ¬a = 0
a₂ : ¬z = 0
a₃ : ¬a * ‖z‖⁻¹ = 1
⊢ ¬a * ‖z‖⁻¹ = -1

Tactic:
rw [toClosedBall_eval_within _ this] at h₁

Premises used: Function.locallyFinsuppWithin.toClosedBall_eval_within
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
h₂ : ¬Eq (α := ℤ) ((D : (a : E) → ℤ) z : ℤ) (0 : ℤ)
a₁ : ¬a = 0
a₂ : ¬z = 0
a₃ : ¬a * ‖z‖⁻¹ = 1
a₄ : ¬a * ‖z‖⁻¹ = -1
⊢ Membership.mem (γ := Set E) (closedBall 0 |a|) z

Tactic:
rw [toClosedBall_eval_within _ this] at h₁

Premises used: Function.locallyFinsuppWithin.toClosedBall_eval_within
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
h₂ : Membership.mem (γ := Set E) (closedBall 0 |b|) z
⊢ ¬Eq (α := ℤ)
      ((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
              locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
            (a : E) → ℤ)
          z :
        ℤ)
      (0 : ℤ)

Tactic:
rwa [toClosedBall_eval_within]

Premises used: Function.locallyFinsuppWithin.toClosedBall_eval_within
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
h₂ : ∀ (this : ‖z‖ ≤ a), ‖z‖ ≤ b
⊢ Membership.mem (γ := Set E) (closedBall 0 |b|) z

Tactic:
simp_all only [abs_of_pos ha, mem_closedBall, dist_zero_right, abs_of_pos hb]

Premises used: Metric.mem_closedBall, abs_of_pos, dist_zero_right
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
linarith : b < ‖z‖ → a - b + (‖z‖ - a) + (b - ‖z‖) = 0
⊢ ‖z‖ ≤ b

Tactic:
linarith
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
⊢ LE.le (α := ℝ) 0 (↑((D : (a : E) → ℤ) 0) : ℝ)

Tactic:
Int.cast_nonneg (hD 0)

Premises used: Int.cast_nonneg, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
⊢ LE.le (α := ℝ) 0 (↑((D : (a : E) → ℤ) 0) : ℝ)

Tactic:
exact Int.cast_nonneg (hD 0)

Premises used: Int.cast_nonneg, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
⊢ (logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D =
    HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) : ℝ → ℝ)
      ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (D - single e 1) : ℝ → ℝ)

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
rw :
  StrictMonoOn
    (HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) : ℝ → ℝ)
      ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (D - single e 1) : ℝ → ℝ))
    (Ioi ‖e‖)
⊢ StrictMonoOn (β := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) (Ioi ‖e‖)

Tactic:
rw [(by aesop : logCounting D = logCounting (single e 1) + logCounting (D - single e 1))]
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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‖)
hg : MonotoneOn (β := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (D - 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‖)

Tactic:
apply StrictMonoOn.add_monotone

Premises used: StrictMonoOn.add_monotone
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
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 : ℝ)
⊢ 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

Premises used: Set.mem_Ioi
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
hf : (↑1 : ℝ) * (log a - log ‖e‖) < (↑1 : ℝ) * (log b - log ‖e‖)
⊢ LT.lt (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) a : ℝ)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)

Tactic:
rw [logCounting_single_eq_log_sub_const ha.le, logCounting_single_eq_log_sub_const hb.le]

Premises used: Function.locallyFinsuppWithin.logCounting_single_eq_log_sub_const, LT.lt.le
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
hf : 0 < a
⊢ (↑1 : ℝ) * (log a - log ‖e‖) < (↑1 : ℝ) * (log b - log ‖e‖)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
⊢ 0 < a

Tactic:
(norm_nonneg e).trans_lt ha

Premises used: LE.le.trans_lt, norm_nonneg
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
⊢ 0 < a

Tactic:
exact (norm_nonneg e).trans_lt ha

Premises used: LE.le.trans_lt, norm_nonneg
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
apply₁ : Membership.mem (γ := Set ℝ) (Ioi 0) a
⊢ LE.le (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (D - single e 1) a : ℝ)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (D - single e 1) b : ℝ)

Tactic:
apply logCounting_mono _ _ ((norm_nonneg e).trans_lt hb) hab

Premises used: Function.locallyFinsuppWithin.logCounting_mono, LE.le.trans_lt, norm_nonneg
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
⊢ 0 ≤ D - single e 1

Tactic:
simp [hD]
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) a

Tactic:
simpa [mem_Ioi] using (norm_nonneg e).trans_lt ha

Premises used: Set.mem_Ioi, LE.le.trans_lt, norm_nonneg
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
f : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f
hr : 1 ≤ r
linarith : r ≤ 0 → -1 + (1 - r) + (r - 0) = 0
⊢ 0 < r

Tactic:
linarith
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
f : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f
hr : 1 ≤ r
⊢ 0 < r

Tactic:
have h₃r : 0 < r := by linarith
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
this :
  ∀ (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‖⁻¹)
⊢ LE.le (α := ℝ) 0 (↑((f : (a : E) → ℤ) 0) : ℝ)

Tactic:
simpa using h 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
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‖⁻¹)
⊢ LE.le (α := ℝ) (0 : ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f r : ℝ)

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)
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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‖⁻¹)
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‖⁻¹)
⊢ 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
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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‖⁻¹)

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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‖⁻¹)
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‖⁻¹)
⊢ 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|

Premises used: abs, Metric.closedBall, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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‖⁻¹)

Tactic:
mul_nonneg ?_ <| log_nonneg ?_

Premises used: mul_nonneg, Real.log_nonneg
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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) :
      ℝ)
pos₁ : 1 ≤ 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:
refine mul_nonneg ?_ <| log_nonneg ?_

Premises used: mul_nonneg, Real.log_nonneg
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
⊢ LE.le (α := ℝ) 0
    (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) f :
              locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
            (a : E) → ℤ)
          a) :
      ℝ)

Tactic:
simpa [h₂a] using h a
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
⊢ 1 ≤ r * ‖a‖⁻¹

Tactic:
simpa [mul_comm r, one_le_inv_mul₀ (norm_pos_iff.mpr h₁a), abs_of_pos h₃r] using h₂a

Premises used: Iff.mpr, norm_pos_iff, one_le_inv_mul₀, mul_comm, abs_of_pos