Successive minima and Minkowski's theorems

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremOrthonormalBasis.volume_weighted_crosspolytope#

The canonical Euclidean volume of a weighted cross-polytope in an arbitrary real basis. The index type may be empty, in which case the volume and the empty products are one.

OrthonormalBasis.volume_weighted_crosspolytope.{u_1, u_2} {ι : Type u_1} {E : Type u_2} [Fintype ι]
  [DecidableEq ι] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] (o : OrthonormalBasis ι ℝ E) (b : Module.Basis ι ℝ E)
  (a : ι → ℝ) (ha : ∀ (i : ι), 0 < a i) :
  MeasureTheory.volume {x | ∑ i, a i * |(b.repr x) i| ≤ 1} =
    ENNReal.ofReal
      (2 ^ Fintype.card ι / ↑(Fintype.card ι).factorial * |o.toBasis.det ⇑b| / ∏ i, a i)

Lean

Formalized in Tau Ceti as OrthonormalBasis.volume_weighted_crosspolytope.

Sources

• Tau Ceti documentation: OrthonormalBasis.volume_weighted_crosspolytope
• Source of OrthonormalBasis.volume_weighted_crosspolytope in TauCeti/MeasureTheory/Measure/Lebesgue/Weighted/Crosspolytope.lean
• Tau Ceti roadmap status: Successive minima and Minkowski's theorems

LeanOrthonormalBasis.volume_weighted_crosspolytope

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.