OAI/Analysis/MassAction/AffineSignGap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem326.Affine.abs_sum_mul_le line 14

   Source documentation

   The elementary sup-norm / one-norm pairing estimate used by active affine labels.

   theorem abs_sum_mul_le (ι : Type uIota) [Fintype ι]
       (u v : ι → ℝ) :
       |∑ i, u i * v i| ≤ ‖u‖ * ∑ i, |v i| := by
   …

2. theorem OAI.Problem326.Affine.sign_gap_of_abs_sub_lt line 28

   Source documentation

   A nonzero linear comparison is stable under an error smaller than half its gap.

   theorem sign_gap_of_abs_sub_lt {a b H : ℝ}
       (hab : |a - b| < |b| / 2) (hH : H ≤ |b| / 2) :
       (0 < a ↔ 0 < b) ∧ (a < 0 ↔ b < 0) ∧ H ≤ |a| := by
   …