mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: n : ℕ
B : ℝ≥0
⊢ {p |
        p.natDegree ≤ n ∧
          ∀ (i : Fin (n + 1)), -(↑(n.choose ↑i) * ↑B) ≤ ↑(p.coeff ↑i) ∧ ↑(p.coeff ↑i) ≤ ↑(n.choose ↑i) * ↑B}.ncard =
    ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)

Tactic:
rw [← boxPoly, ncard_boxPoly]

Goal state after:
n : ℕ
B : ℝ≥0
⊢ ∏ i, (⌊↑(n.choose ↑i) * ↑B⌋ - ⌈-(↑(n.choose ↑i) * ↑B)⌉ + 1).toNat = ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: n : ℕ
B : ℝ≥0
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ 0 ≤ 2 * ⌊↑(n.choose ↑i) * ↑B⌋ + 1

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: n : ℕ
B : ℝ≥0
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ 0 ≤ ↑(n.choose ↑i) * ↑B

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R ℂ
n : ℕ
hn : n = 0
⊢ (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1

Tactic:
simp [hn]

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz : z ∈ p.aroots ℂ
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K :=
  { to_charZero := IntermediateField.charZero ℚ⟮z⟯,
    to_finiteDimensional := adjoin.finiteDimensional (IsIntegral.tower_top (isIntegral_of_mahlerMeasure_eq_one h hz)) }
y : ↥K := ⟨z, ⋯⟩
φ : ↥K →+* ℂ
⊢ φ y ∈ p.aroots ℂ

Tactic:
mem_aroots

Goal state after:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz✝ : z ∈ p.aroots ℂ
hz : p ≠ 0 ∧ (aeval z) p = 0
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K :=
  { to_charZero := IntermediateField.charZero ℚ⟮z⟯,
    to_finiteDimensional := adjoin.finiteDimensional (IsIntegral.tower_top (isIntegral_of_mahlerMeasure_eq_one h hz✝)) }
y : ↥K := ⟨z, ⋯⟩
φ : ↥K →+* ℂ
⊢ p ≠ 0 ∧ (aeval (φ y)) p = 0
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: case insert.inr.e_a
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
i : ι
t : Finset ι
hi : i ∉ t
IH : (∏ i ∈ t, f i) ∣[∑ i ∈ t, k i] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#t) - 1) • ∏ i ∈ t, f i ∣[k i] g
ht : t.Nonempty
⊢ |↑(Matrix.GeneralLinearGroup.det g)| * |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#t) - 1) =
    |↑(Matrix.GeneralLinearGroup.det g)| ^ ↑(#t)

Tactic:
nth_rw 2 [show (#t : ℤ) = 1 + (#t - 1) by grind]

Goal state after:
case insert.inr.e_a
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
i : ι
t : Finset ι
hi : i ∉ t
IH : (∏ i ∈ t, f i) ∣[∑ i ∈ t, k i] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#t) - 1) • ∏ i ∈ t, f i ∣[k i] g
ht : t.Nonempty
⊢ |↑(Matrix.GeneralLinearGroup.det g)| * |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#t) - 1) =
    |↑(Matrix.GeneralLinearGroup.det g)| ^ (1 + (↑(#t) - 1))
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mpr.refine_2
a : SL(2, ℤ)
⊢ (mapGL ℝ) (a * ModularGroup.T * a⁻¹) • OnePoint.map Rat.cast ((mapGL ℚ) a • ∞) =
    OnePoint.map Rat.cast ((mapGL ℚ) a • ∞)

Tactic:
rw [← Rat.coe_castHom, ← (Rat.castHom ℝ).algebraMap_toAlgebra]

Goal state after:
case mpr.refine_2
a : SL(2, ℤ)
⊢ (mapGL ℝ) (a * ModularGroup.T * a⁻¹) • OnePoint.map (⇑(algebraMap ℚ ℝ)) ((mapGL ℚ) a • ∞) =
    OnePoint.map (⇑(algebraMap ℚ ℝ)) ((mapGL ℚ) a • ∞)
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mpr
c : OnePoint ℝ
⊢ (∃ g, c = (mapGL ℝ) g • ∞) → c ∈ Set.range (OnePoint.map Rat.cast)

Tactic:
rintro ⟨g, rfl⟩
    refine ⟨mapGL ℚ g • ∞, ?_⟩
    rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty,
       ← (Rat.castHom ℝ).algebraMap_toAlgebra, g.map_mapGL]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mpr
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp : g.IsParabolic
hgi : ↑g 1 0 = 0
⊢ ∃ a, ¬a = 0 ∧ upperRightHom a ∈ 𝒢

Tactic:
rw [Subgroup.HasDetPlusMinusOne.isParabolic_iff_of_upperTriangular hgg hgi] at hgp

Goal state after:
case mpr
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp : (∃ x, x ≠ 0 ∧ g = upperRightHom x) ∨ ∃ x, x ≠ 0 ∧ g = -upperRightHom x
hgi : ↑g 1 0 = 0
⊢ ∃ a, ¬a = 0 ∧ upperRightHom a ∈ 𝒢
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.periods
inst✝ : 𝒢.HasDetPlusMinusOne
this : DiscreteTopology ↥𝒢.adjoinNegOne.strictPeriods
⊢ 0 < 𝒢.adjoinNegOne.strictWidthInfty ↔ IsCusp ∞ 𝒢

Tactic:
strictWidthInfty_pos_iff,

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.periods
inst✝ : 𝒢.HasDetPlusMinusOne
this : DiscreteTopology ↥𝒢.adjoinNegOne.strictPeriods
⊢ IsCusp ∞ 𝒢.adjoinNegOne ↔ IsCusp ∞ 𝒢
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: f : ℍ → ℂ
hf : MDiff f
k : ℤ
g : GL (Fin 2) ℝ
hg : (↑g).det < 0
⊢ MDiff (f ∣[k] g)

Tactic:
rw [show g = J * (J * g) by simp [← mul_assoc, ← sq], SlashAction.slash_mul]

Goal state after:
f : ℍ → ℂ
hf : MDiff f
k : ℤ
g : GL (Fin 2) ℝ
hg : (↑g).det < 0
⊢ MDiff ((f ∣[k] J) ∣[k] (J * g))
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ (b : ℝ), y ≤ b → ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
τ : ℍ
⊢ τ.im ^ t ≠ 0

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: E✝ : Type u_1
inst✝ : SeminormedAddCommGroup E✝
f : ℍ → E✝
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ (b : ℝ), y ≤ b → ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
hfm : ContinuousOn (fun τ ↦ ‖f τ‖ / τ.im ^ t) (truncatedFundamentalDomain y)
E : ℝ
hE : ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / τ.im ^ t ≤ E
τ : ℍ
hτ : τ ∈ 𝒟
hτ' : y ≤ τ.im
⊢ 0 ≤ τ.im ^ t

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
this : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
hI :
  f (S • UpperHalfPlane.I) =
    denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S)) ↑UpperHalfPlane.I ^
        k *
      f UpperHalfPlane.I
h2I2 :
  f (S • ⟨2, ⋯⟩ • UpperHalfPlane.I) =
    denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S))
          ↑(⟨2, ⋯⟩ • UpperHalfPlane.I) ^
        k *
      f (⟨2, ⋯⟩ • UpperHalfPlane.I)
⊢ k = 0 ∨ c = 0

Tactic:
sl_moeb,

Goal state after:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
this : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
hI :
  f (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S) • UpperHalfPlane.I) =
    denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S)) ↑UpperHalfPlane.I ^
        k *
      f UpperHalfPlane.I
h2I2 :
  f
      (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S) •
        ⟨2, ⋯⟩ • UpperHalfPlane.I) =
    denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S))
          ↑(⟨2, ⋯⟩ • UpperHalfPlane.I) ^
        k *
      f (⟨2, ⋯⟩ • UpperHalfPlane.I)
⊢ k = 0 ∨ c = 0
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: E✝ : Type u_1
inst✝ : SeminormedAddCommGroup E✝
f : ℍ → E✝
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ (b : ℝ), y ≤ b → ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
hfm : ContinuousOn (fun τ ↦ ‖f τ‖ / τ.im ^ t) (truncatedFundamentalDomain y)
E : ℝ
hE : ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / τ.im ^ t ≤ E
τ : ℍ
hτ : τ ∈ 𝒟
hτ' : τ.im ≤ y
⊢ 0 < τ.im ^ t

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg : g • τ ∈ 𝒟
⊢ 0 < (g • τ).im ^ t

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f τ‖ / (g • τ).im ^ t ≤ F
hg : g • τ ∈ 𝒟
⊢ 0 ≤ ‖f τ‖ / (g • τ).im ^ t

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
⊢ 0 < 2 * π * t

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : ∀ (g : SL(2, ℤ)), (fun τ ↦ f (g • τ)) =O[atImInfty] fun z ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst✝ : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
f' : ℍ → SL(2, ℤ) ⧸ Γ → E := fun τ ↦ Quotient.lift (fun g ↦ f (g⁻¹ • τ)) ⋯
hf'_cont : ∀ (γ : SL(2, ℤ) ⧸ Γ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ f' x γ
hf'_inv : ∀ (τ : ℍ) (g : SL(2, ℤ)) (γ : SL(2, ℤ) ⧸ Γ), f' (g • τ) (g • γ) = f' τ γ
hf'_infty : ∀ (γ : SL(2, ℤ) ⧸ Γ), (fun x ↦ f' x γ) =O[atImInfty] fun z ↦ z.im ^ t
this : Fintype (SL(2, ℤ) ⧸ Γ)
C : ℝ
hC : ∀ (τ : ℍ), ‖∑ c, ‖f' τ c‖‖ ≤ C * max τ.im (1 / τ.im) ^ t
τ : ℍ
⊢ 0 ≤ ∑ γ, ‖f' τ γ‖

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty

Goal state before:
pp: k : ℤ
hk : 3 ≤ k
z : ℍ
hk' : 2 < ↑k
b : Fin 2 → ℤ
⊢ 0 ≤ ↑k

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : CuspFormClass F Γ k
f : F
C : ℝ
τ : ℍ
hC : ‖petersson k (⇑f) (⇑f) τ‖ ≤ C
⊢ 0 ≤ ‖f τ‖

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : CuspFormClass F Γ k
f : F
C : ℝ
τ : ℍ
hC : ‖petersson k (⇑f) (⇑f) τ‖ ≤ C
⊢ 0 ≤ √C / τ.im ^ (↑k / 2)

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence

Goal state before:
pp: k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : 2 < ↑k
p_sum : Summable fun x ↦ ‖↑x‖ ^ (-k)
K : Set ℍ
hK : IsCompact K
A B : ℝ
hB : 0 < B
HABK : K ⊆ verticalStrip A B
p : ↑(gammaSet N 1 a)
z : ℍ
hz : z ∈ verticalStrip A B
⊢ 0 ≤ ↑k

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖petersson (↑k) (⇑f) (⇑f) τ‖ ≤ C * max τ.im (1 / τ.im) ^ ↑k
⊢ 0 ≤ ‖petersson (↑k) (⇑f) (⇑f) τ‖ / max τ.im (1 / τ.im) ^ ↑k

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖petersson (↑k) (⇑f) (⇑f) τ‖ ≤ C * max τ.im (1 / τ.im) ^ ↑k
⊢ 0 < max τ.im (1 / τ.im) ^ ↑k

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h : 0 < ‖↑τ.im ^ ↑k‖
⊢ 0 ≤ ‖f τ‖

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h : 0 < ‖↑τ.im ^ ↑k‖
⊢ 0 ≤ √C * max 1 (1 / τ.im ^ ↑k)

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h✝ : 0 < ‖↑τ.im ^ ↑k‖
t : NNReal
h : τ.im = ↑t
ht : 0 < t
⊢ 0 ≤ ‖↑(t ^ k)‖₊

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
⊢ 0 < 1 / ↑n

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
⊢ 0 ≤ h

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
x : ℝ
⊢ 0 < (↑x + 1 / ↑n * I).im

Tactic:
simp [hn]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F✝ : Type u_2
inst✝¹ : FunLike F✝ ℍ ℂ
inst✝ : ModularFormClass F✝ Γ k
f : F✝
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
F : ℝ → ℝ := fun x ↦ ‖1 / ↑h * (1 / 𝕢 h (↑x + 1 / ↑n * I) ^ n * f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ })‖
⊢ 0 ≤ ↑n ^ e

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
a : (x : ℕ+) × ↥(↑x).divisorsAntidiagonal
⊢ 0 ≤ ‖↑(↑a.snd).2 ^ k * r ^ ((↑a.snd).1 * (↑a.snd).2)‖

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F✝ : Type u_2
inst✝¹ : FunLike F✝ ℍ ℂ
inst✝ : ModularFormClass F✝ Γ k
f : F✝
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this✝ : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
F : ℝ → ℝ := fun x ↦ ‖1 / ↑h * (1 / 𝕢 h (↑x + 1 / ↑n * I) ^ n * f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ })‖
hne : ‖↑n ^ e‖ = ↑n ^ e
this : ∀ (x : ℝ), F x ≤ 1 / h * (1 / Real.exp (-2 * Real.pi / h)) * (C * ↑n ^ e)
⊢ 0 ≤ h

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), ‖f τ‖ ≤ C * max 1 (1 / τ.im ^ k)
τ : ℍ
hτ : τ.im ≤ 1
⊢ 0 ≤ (τ.im ^ k)⁻¹

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), ‖f τ‖ ≤ C * max 1 (1 / τ.im ^ k)
τ : ℍ
hτ : τ.im ≤ 1
⊢ 0 < τ.im ^ k

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : CuspFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), ‖f τ‖ ≤ C / τ.im ^ (↑k / 2)
τ : ℍ
⊢ 0 ≤ τ.im ^ (-(↑k / 2))

Tactic:
positivity

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
⊢ 0 ≤ x

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: n : ℕ
z : ℂ
hz : z ∈ ℍₒ
h : 1 = cexp (2 * ↑π * I * (↑n + 1) * z)
⊢ 0 < ↑n + 1

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case hf
z : ℍ
⊢ HasSum (fun n ↦ ∑' (m : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2) ((↑z ^ 2)⁻¹ * G2 (S • z)) (symmetricIco ℤ)

Tactic:
rw [hasSum_symmetricIco_int_iff]

Goal state after:
case hf
z : ℍ
⊢ Tendsto (fun N ↦ ∑ n ∈ Finset.Ico (-↑N) ↑N, ∑' (m : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2) atTop (𝓝 ((↑z ^ 2)⁻¹ * G2 (S • z)))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case mul
γ g h : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
hy✝ : h ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
ih : G2 ∣[2] h = G2 - D2 h
⊢ G2 ∣[2] (g * h) = G2 - D2 (g * h)

Tactic:
| mul g h _ _ ig ih =>

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
hdet : ↑(Matrix.GeneralLinearGroup.det g) = (↑g).det
hdetℂ : ↑(↑g).det ≠ 0
hσ : ∀ (x : ℂ), (σ g) x = x
z : ℍ
hz : denom g ↑z ≠ 0
h_smul : HasDerivAt (fun w ↦ ↑(g • ↑ofComplex w)) (↑(↑g).det / denom g ↑z ^ 2) ↑z
h_F : HasDerivAt (F ∘ ↑ofComplex) (deriv (F ∘ ↑ofComplex) ↑(g • ↑ofComplex ↑z)) ↑(g • ↑ofComplex ↑z)
h_denom : HasDerivAt (fun w ↦ denom g w ^ (-k)) (-↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1)) ↑z
hcomp :
  F ∣[k] g ∘ ↑ofComplex =ᶠ[𝓝 ↑z] fun w ↦ ↑(↑g).det ^ (k - 1) * ((F ∘ ↑ofComplex) ↑(g • ↑ofComplex w) * denom g w ^ (-k))
⊢ (2 * ↑π * I)⁻¹ *
      (↑(↑g).det ^ (k - 1) *
        (deriv (F ∘ ↑ofComplex) ↑(g • z) * (↑(↑g).det / denom g ↑z ^ 2) * denom g ↑z ^ (-k) +
          F (g • z) * (-↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1)))) =
    (↑(↑g).det)⁻¹ *
        ((2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑(g • z) * (↑(↑g).det ^ (k - 1) * ↑(↑g).det ^ 2) *
          (denom g ↑z ^ (-k) * denom g ↑z ^ (-2))) -
      ↑k * (2 * ↑π * I)⁻¹ * (↑(↑g 1 0) / denom g ↑z) * (F (g • z) * ↑(↑g).det ^ (k - 1) * denom g ↑z ^ (-k))

Tactic:
zpow_sub_one₀ hz

Goal state after:
k : ℤ
F : ℍ → ℂ
hF : MDiff F
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
hdet : ↑(Matrix.GeneralLinearGroup.det g) = (↑g).det
hdetℂ : ↑(↑g).det ≠ 0
hσ : ∀ (x : ℂ), (σ g) x = x
z : ℍ
hz : denom g ↑z ≠ 0
h_smul : HasDerivAt (fun w ↦ ↑(g • ↑ofComplex w)) (↑(↑g).det / denom g ↑z ^ 2) ↑z
h_F : HasDerivAt (F ∘ ↑ofComplex) (deriv (F ∘ ↑ofComplex) ↑(g • ↑ofComplex ↑z)) ↑(g • ↑ofComplex ↑z)
h_denom : HasDerivAt (fun w ↦ denom g w ^ (-k)) (-↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1)) ↑z
hcomp :
  F ∣[k] g ∘ ↑ofComplex =ᶠ[𝓝 ↑z] fun w ↦ ↑(↑g).det ^ (k - 1) * ((F ∘ ↑ofComplex) ↑(g • ↑ofComplex w) * denom g w ^ (-k))
⊢ (2 * ↑π * I)⁻¹ *
      (↑(↑g).det ^ (k - 1) *
        (deriv (F ∘ ↑ofComplex) ↑(g • z) * (↑(↑g).det / denom g ↑z ^ 2) * denom g ↑z ^ (-k) +
          F (g • z) * (-↑k * ↑(↑g 1 0) * (denom g ↑z ^ (-k) * (denom g ↑z)⁻¹)))) =
    (↑(↑g).det)⁻¹ *
        ((2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑(g • z) * (↑(↑g).det ^ (k - 1) * ↑(↑g).det ^ 2) *
          (denom g ↑z ^ (-k) * denom g ↑z ^ (-2))) -
      ↑k * (2 * ↑π * I)⁻¹ * (↑(↑g 1 0) / denom g ↑z) * (F (g • z) * ↑(↑g).det ^ (k - 1) * denom g ↑z ^ (-k))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
N a : ℕ
⊢ 0 < ↑a + 1

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: c✝ : OnePoint ℝ
hc : IsCusp c✝ (Matrix.SpecialLinearGroup.mapGL ℝ).range
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [OnePoint.isZeroAt_iff_forall_SL2Z hc]

Goal state after:
c✝ : OnePoint ℝ
hc : IsCusp c✝ (Matrix.SpecialLinearGroup.mapGL ℝ).range
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)