Heights of points in projective space

We define the multiplicative (Projectivization.mulHeight) and the logarithmic (Projectivization.logHeight) height of a point in a (finite-dimensional) projective space over a field that has a Height.AdmissibleAbsValues instance.

The height is defined to be the height of any representative tuple; it does not depend on which representative is chosen.

noncomputable def Projectivization.mulHeight {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : Projectivization K (ι → K)) : ℝ

The multiplicative height of a point on a finite-dimensional projective space over K with a given basis.

Equations

• x.mulHeight = Projectivization.lift (fun (r : { v : ι → K // v ≠ 0 }) => Height.mulHeight ↑r) ⋯ x

noncomputable def Projectivization.logHeight {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : Projectivization K (ι → K)) : ℝ

The logarithmic height of a point on a finite-dimensional projective space over K with a given basis.

Equations

• x.logHeight = Projectivization.lift (fun (r : { v : ι → K // v ≠ 0 }) => Height.logHeight ↑r) ⋯ x

theorem Projectivization.mulHeight_mk {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] {x : ι → K} (hx : x ≠ 0) : (mk K x hx).mulHeight = Height.mulHeight x

theorem Projectivization.logHeight_mk {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] {x : ι → K} (hx : x ≠ 0) : (mk K x hx).logHeight = Height.logHeight x

theorem Projectivization.logHeight_eq_log_mulHeight {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : Projectivization K (ι → K)) : x.logHeight = Real.log x.mulHeight

theorem Projectivization.one_le_mulHeight {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : Projectivization K (ι → K)) : 1 ≤ x.mulHeight

theorem Projectivization.mulHeight_pos {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : Projectivization K (ι → K)) : 0 < x.mulHeight

theorem Projectivization.mulHeight_ne_zero {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : Projectivization K (ι → K)) : x.mulHeight ≠ 0

theorem Projectivization.logHeight_nonneg {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : Projectivization K (ι → K)) : 0 ≤ x.logHeight

def Mathlib.Meta.Positivity.evalProjMulHeight : PositivityExt

Extension for the positivity tactic: Projectivization.mulHeight is always positive.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Meta.Positivity.evalProjLogHeight : PositivityExt

Extension for the positivity tactic: Projectivization.logHeight is always nonnegative.

Equations

• One or more equations did not get rendered due to their size.