Unit radial cone estimates extend to both orientations and the vertex

Proved

BianchiIX.homogeneous_cone_of_unit

by trppppp · Nov 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

bianchi-ix-era-statisticsdynamical-systems

Let $D:\mathbb R^3\to\mathbb R^3$ be linear and $R>0$ . Suppose every $z$ with $Rz_0=1$ , $|z_1|\leq a$ , $|z_2|\leq b$ satisfies $(Dz)_0\geq0$ , $|(Dz)_1|\leq A(Dz)_0$ , and $|(Dz)_2|\leq B(Dz)_0$ . Then every $v$ satisfying $|v_1|\leq a|Rv_0|$ , $|v_2|\leq b|Rv_0|$ obeys

|(Dv)_1|\leq A|(Dv)_0|,\qquad |(Dv)_2|\leq B|(Dv)_0|.

Preamble

import Mathlib.Analysis.Normed.Operator.Basic
import Mathlib.LinearAlgebra.Matrix.Notation
import Mathlib.Tactic.FinCases
import Mathlib.Tactic.Ring
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Positivity

namespace BianchiIX
end BianchiIX

noncomputable section
open BianchiIX

Formal statement

theorem BianchiIX.homogeneous_cone_of_unit
    (D : (Fin 3 → ℝ) →L[ℝ] (Fin 3 → ℝ)) {R a b A B : ℝ} (hR : 0 < R)
    (hunit : ∀ z : Fin 3 → ℝ, R * z 0 = 1 → |z 1| ≤ a → |z 2| ≤ b →
      0 ≤ D z 0 ∧ |D z 1| ≤ A * D z 0 ∧ |D z 2| ≤ B * D z 0)
    (v : Fin 3 → ℝ) (hva : |v 1| ≤ a * |R * v 0|) (hvb : |v 2| ≤ b * |R * v 0|) :
    |D v 1| ≤ A * |D v 0| ∧ |D v 2| ≤ B * |D v 0| := by sorry

Source

https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/blob/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX/Analysis/HomogeneousCone.lean#L9-L48

View graph