Reduction.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Cone-volume identities.

theorem OAI.GeneralMahler.Body.vol_pos line 12
theorem OAI.GeneralMahler.Body.chi_axis line 18
Source documentation
Slice integral of a cone at a vertical dual vector.
```
theorem chi_axis (K : Body n) (r : ℝ) (hr : 0 < r) :
    chi K.cone (pair r 0) =
      (r⁻¹ ^ (n+1)) * n.factorial * (volume (K : Set (Rn n))).toReal := by
…
```
Mentions: OAI.GeneralMahler.Body, OAI.GeneralMahler.chi, OAI.GeneralMahler.pair, OAI.GeneralMahler.Rn
def OAI.GeneralMahler.Body.shear line 81
Source documentation
Shear of cone coordinates for translations.
```
def shear (z : Rn n) : (LiftSpace n) ≃ₗ[ℝ] LiftSpace n where
…
```
Mentions: OAI.GeneralMahler.Rn, OAI.GeneralMahler.LiftSpace
theorem OAI.GeneralMahler.Body.shear_off line 92
theorem OAI.GeneralMahler.Body.cone_volume line 110