mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : ¬0 < ↑(Matrix.GeneralLinearGroup.det g)
this : {h | ¬0 < ↑(Matrix.GeneralLinearGroup.det h)} ∈ 𝓝 g
h : GL (Fin 2) ℝ
hh : ¬0 < ↑(Matrix.GeneralLinearGroup.det h)
⊢ σ h = σ g

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : ¬0 < ↑(Matrix.GeneralLinearGroup.det g)
this : {h | ¬0 < ↑(Matrix.GeneralLinearGroup.det h)} ∈ 𝓝 g
⊢ σ =ᶠ[𝓝 g] fun x ↦ σ g

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : ↑(Matrix.GeneralLinearGroup.det g) < 0
⊢ Continuous fun h ↦ ↑(Matrix.GeneralLinearGroup.det h)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: g : GL (Fin 2) ℝ
⊢ σ =ᶠ[𝓝 g] fun x ↦ σ g

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: g : GL (Fin 2) ℝ
τ : ℍ
⊢ ∀ (a : GL (Fin 2) ℝ × ℍ),
    σ a.1 = σ g → (σ g) (num a.1 ↑a.2 / denom a.1 ↑a.2) = (σ a.1) (num a.1 ↑a.2 / denom a.1 ↑a.2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: g : GL (Fin 2) ℝ
τ : ℍ
⊢ (fun x ↦ (σ g) (num x.1 ↑x.2 / denom x.1 ↑x.2)) =ᶠ[nhds (g, τ)] fun x ↦ (σ x.1) (num x.1 ↑x.2 / denom x.1 ↑x.2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: ⊢ ContinuousSMul (GL (Fin 2) ℝ) ℍ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ circleAverage (fun x ↦ log⁺ ‖∑ c ∈ s, f c x‖) 0 r ≤ circleAverage (fun x ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card) 0 r

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ s)) → IsOpen[inst✝¹] s
⊢ CompactlyGeneratedSpace X

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: K : Set ℍ
hK : IsCompact K
⊢ ∃ A, ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: K : Set ℍ
hK : IsCompact K
⊢ !![0, -1; 1, 0].det = 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : WeaklyLocallyCompactSpace X
⊢ CompactlyGeneratedSpace X

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ circleAverage (fun x ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card) 0 r =
    ∑ c ∈ s, circleAverage (fun x ↦ log⁺ ‖f c x‖) 0 r + log ↑s.card

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: K : Set ℍ
hK : IsCompact K
S : SL(2, ℝ) := ⟨!![0, -1; 1, 0], ⋯⟩
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ S • K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A
g : SL(2, ℝ)
hg : g • I ∈ K
⊢ (S * g) • I ∈ S • K

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
⊢ proximity (∑ a ∈ s, f a) ⊤ ≤ ∑ a ∈ s, proximity (f a) ⊤ + fun x ↦ log ↑s.card

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f₁ f₂ : ℂ → E
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
i : Fin (Nat.succ 0).succ
⊢ i ∈ Finset.univ → Meromorphic (![f₁, f₂] i)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f₁ f₂ : ℂ → E
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ proximity (f₁ + f₂) ⊤ ≤ proximity f₁ ⊤ + proximity f₂ ⊤ + fun x ↦ log 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ proximity (f₁ * f₂) ⊤ = circleAverage (fun x ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: K : Set ℍ
hK : IsCompact K
⊢ ∃ A, ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: ⊢ Continuous fun g ↦ g • I

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ circleAverage (fun x ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0 ≤ circleAverage (fun x ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ circleAverage (fun x ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 =
    circleAverage (fun x ↦ log⁺ ‖f₁ x‖) 0 + circleAverage (fun x ↦ log⁺ ‖f₂ x‖) 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ circleAverage (fun x ↦ log⁺ ‖f₁ x‖) 0 + circleAverage (fun x ↦ log⁺ ‖f₂ x‖) 0 = proximity f₁ ⊤ + proximity f₂ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ proximity (f₁ * f₂) ⊤ ≤ proximity f₁ ⊤ + proximity f₂ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ proximity (f₁ * f₂) 0 ≤ proximity f₁⁻¹ ⊤ + proximity f₂⁻¹ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ proximity f₁⁻¹ ⊤ + proximity f₂⁻¹ ⊤ = proximity f₁ 0 + proximity f₂ 0

Tactic:
proximity_inv,

Goal state after:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ proximity f₁ 0 + proximity f₂⁻¹ ⊤ = proximity f₁ 0 + proximity f₂ 0
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ proximity f₁⁻¹ ⊤ + proximity f₂⁻¹ ⊤ = proximity f₁ 0 + proximity f₂ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ proximity (f₁ * f₂) 0 ≤ proximity f₁ 0 + proximity f₂ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f : ℂ → ℂ
n : ℕ
⊢ proximity (f ^ n) ⊤ = n • proximity f ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f : ℂ → ℂ
n : ℕ
⊢ proximity (f ^ n) 0 = n • proximity f 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: K : Set ℍ
hK : IsCompact K
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
A' : ℝ
hA' : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A'
this✝ : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
⊢ IsCompact {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : CompactlyCoherentSpace X
⊢ CompactlyGeneratedSpace X

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: K : Set ℍ
hK : IsCompact K
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
A' : ℝ
hA' : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A'
this✝² : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this✝¹ : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
this✝ : IsCompact {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
this : IsCompact (Subtype.val ⁻¹' {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'})
⊢ Continuous fun g ↦ g • I

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
⊢ characteristic f ⊤ - characteristic f⁻¹ ⊤ = proximity f ⊤ - proximity f⁻¹ ⊤ - (logCounting f⁻¹ ⊤ - logCounting f ⊤)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
⊢ proximity f ⊤ - proximity f⁻¹ ⊤ - (logCounting f⁻¹ ⊤ - logCounting f ⊤) =
    circleAverage (fun x ↦ log ‖f x‖) 0 - (logCounting f⁻¹ ⊤ - logCounting f ⊤)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
⊢ circleAverage (fun x ↦ log ‖f x‖) 0 - (logCounting f⁻¹ ⊤ - logCounting f ⊤) =
    circleAverage (fun x ↦ log ‖f x‖) 0 - (logCounting f 0 - logCounting f ⊤)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
⊢ circleAverage (fun x ↦ log ‖f x‖) 0 - (logCounting f 0 - logCounting f ⊤) =
    circleAverage (fun x ↦ log ‖f x‖) 0 - Function.locallyFinsuppWithin.logCounting (divisor f Set.univ)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
⊢ characteristic f ⊤ - characteristic f⁻¹ ⊤ =
    circleAverage (fun x ↦ log ‖f x‖) 0 - Function.locallyFinsuppWithin.logCounting (divisor f Set.univ)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
⊢ characteristic f ⊤ R - characteristic f⁻¹ ⊤ R = (characteristic f ⊤ - characteristic f⁻¹ ⊤) R

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
⊢ (characteristic f ⊤ - characteristic f⁻¹ ⊤) R =
    circleAverage (fun x ↦ log ‖f x‖) 0 R - Function.locallyFinsuppWithin.logCounting (divisor f Set.univ) R

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
⊢ closedBall 0 |R| ⊆ Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscrete ℂ] g
hr : r ≠ 0
⊢ characteristic f a r = characteristic g a r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
h : Meromorphic f
a₀ : E
⊢ characteristic f ⊤ - characteristic (fun x ↦ f x - a₀) ⊤ = proximity f ⊤ - proximity (fun x ↦ f x - a₀) ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
a : WithTop E
x✝ : ℝ
hr : 1 ≤ x✝
⊢ 0 x✝ ≤ characteristic f a x✝

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
a : WithTop E
⊢ 0 ≤ᶠ[atTop] characteristic f a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
⊢ circleAverage (fun x ↦ log ‖f x‖) 0 R - Function.locallyFinsuppWithin.logCounting (divisor f Set.univ) R =
    log ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
⊢ characteristic f ⊤ R - characteristic f⁻¹ ⊤ R = log ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
⊢ characteristic f ⊤ 0 - characteristic f⁻¹ ⊤ 0 = (characteristic f ⊤ - characteristic f⁻¹ ⊤) 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
⊢ proximity (∑ a ∈ s, f a) ⊤ r + logCounting (∑ a ∈ s, f a) ⊤ r ≤
    (∑ a ∈ s, proximity (f a) ⊤) r + log ↑s.card + (∑ a ∈ s, logCounting (f a) ⊤) r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
⊢ (∑ a ∈ s, proximity (f a) ⊤) r + log ↑s.card + (∑ a ∈ s, logCounting (f a) ⊤) r =
    (∑ a ∈ s, proximity (f a) ⊤) r + (∑ a ∈ s, logCounting (f a) ⊤) r + log ↑s.card

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
⊢ (∑ a ∈ s, proximity (f a) ⊤) r + (∑ a ∈ s, logCounting (f a) ⊤) r + log ↑s.card =
    ∑ x ∈ s, (proximity (f x) ⊤ r + logCounting (f x) ⊤ r) + log ↑s.card

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
⊢ characteristic (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, characteristic (f a) ⊤) r + log ↑s.card

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
⊢ (characteristic f ⊤ - characteristic f⁻¹ ⊤) 0 =
    circleAverage (fun x ↦ log ‖f x‖) 0 0 - Function.locallyFinsuppWithin.logCounting (divisor f Set.univ) 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
⊢ characteristic (∑ a ∈ s, f a) ⊤ ≤ᶠ[atTop] ∑ a ∈ s, characteristic (f a) ⊤ + fun x ↦ log ↑s.card

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
⊢ circleAverage (fun x ↦ log ‖f x‖) 0 0 - Function.locallyFinsuppWithin.logCounting (divisor f Set.univ) 0 = log ‖f 0‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f₁ f₂ : ℂ → E
r : ℝ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
hr : 1 ≤ r
⊢ ∀ a ∈ Finset.univ, Meromorphic (![f₁, f₂] a)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
⊢ characteristic f ⊤ 0 - characteristic f⁻¹ ⊤ 0 = log ‖f 0‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f₁ f₂ : ℂ → E
r : ℝ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
hr : 1 ≤ r
⊢ characteristic (f₁ + f₂) ⊤ r ≤ characteristic f₁ ⊤ r + characteristic f₂ ⊤ r + log 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f₁ f₂ : ℂ → E
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ characteristic (f₁ + f₂) ⊤ ≤ᶠ[atTop] characteristic f₁ ⊤ + characteristic f₂ ⊤ + fun x ↦ log 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
⊢ |characteristic f ⊤ R - characteristic f⁻¹ ⊤ R| ≤ max |log ‖f 0‖| |log ‖meromorphicTrailingCoeffAt f 0‖|

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤
⊢ characteristic (f₁ * f₂) 0 r ≤ (characteristic f₁ 0 + characteristic f₂ 0) r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
⊢ locallyFinsupp E ℤ →+ locallyFinsuppWithin (closedBall 0 |r|) ℤ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: K : Set ℍ
hK : IsCompact K
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
A' : ℝ
hA' : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A'
this✝² : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this✝¹ : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
this✝ : IsCompact {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
this : IsCompact (Subtype.val ⁻¹' {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'})
g : { A // A.det = 1 }
hg : g ∈ (fun g ↦ g • I) ⁻¹' K
j : Fin 2
⊢ |↑g ((fun i ↦ i) ⟨0, ⋯⟩) j| ^ 2 ≤ ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
z : E
f : locallyFinsupp E ℤ
ha : z ∈ closedBall 0 |r|
⊢ ((toClosedBall r) f) z = f z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
R : ℝ
⊢ ‖(characteristic f ⊤ - characteristic f⁻¹ ⊤) R‖ ≤ max |log ‖f 0‖| |log ‖meromorphicTrailingCoeffAt f 0‖| * ‖1 R‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: r : ℝ
f : ℂ → ℂ
h : Meromorphic f
⊢ divisor f (closedBall 0 |r|) = (toClosedBall r) (divisor f univ)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤
⊢ characteristic (f₁ * f₂) 0 ≤ᶠ[atTop] characteristic f₁ 0 + characteristic f₂ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E : Type u_2
inst✝ : NormedAddCommGroup E
r : ℝ
f : locallyFinsupp E ℤ
⊢ ((toClosedBall r) f).support ⊆ closedBall 0 |r|

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
⊢ (fun r ↦ ∑ᶠ (z : E), ↑(((toClosedBall r) 0) z) * log (r * ‖z‖⁻¹) + ↑(0 0) * log r) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r A B C D : ℝ
⊢ A + B + (C + D) = A + C + (B + D)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤
⊢ characteristic (f₁ * f₂) ⊤ r ≤ (characteristic f₁ ⊤ + characteristic f₂ ⊤) r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
⊢ (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤
⊢ characteristic (f₁ * f₂) ⊤ ≤ᶠ[atTop] characteristic f₁ ⊤ + characteristic f₂ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: f : ℂ → ℂ
n : ℕ
hf : Meromorphic f
⊢ characteristic (f ^ n) 0 = n • characteristic f 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: f : ℂ → ℂ
n : ℕ
hf : Meromorphic f
⊢ characteristic (f ^ n) ⊤ = n • characteristic f ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: K : Set ℍ
hK : IsCompact K
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
A' : ℝ
hA' : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A'
this✝² : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this✝¹ : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
this✝ : IsCompact {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
this : IsCompact (Subtype.val ⁻¹' {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'})
g : { A // A.det = 1 }
hg : g ∈ (fun g ↦ g • I) ⁻¹' K
j : Fin 2
⊢ |↑g ((fun i ↦ i) ⟨1, ⋯⟩) j| ^ 2 ≤ ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: ⊢ IsProperMap fun g ↦ g • I

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: 𝒢 : Subgroup SL(2, ℝ)
inst✝ : DiscreteTopology ↥𝒢
⊢ ProperlyDiscontinuousSMul ↥𝒢 ℍ

Tactic:
by

Goal state after: