Arithmetic.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Numerical consequences, to be used only after the geometric volume identities.

theorem OAI.ProjectionCounterexample.sum_positive_eq_half_sum_abs line 15
Source documentation
Algebraic double-counting identity used after the visible-face measure sum. The balance condition is later proved from the actual simplex facet vectors.
```
theorem sum_positive_eq_half_sum_abs {ι : Type*} [Fintype ι]
    (a : ι → ℝ) (ha : ∑ i, a i = 0) :
    (∑ i with 0 < a i, a i) = (∑ i, |a i|) / 2 := by
…
```
theorem OAI.ProjectionCounterexample.numerical_product_ratio line 32
theorem OAI.ProjectionCounterexample.numerical_strict_excess line 38