OAI/Combinatorics/Permanent/Norm.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FourRow.scalar_rpow_lower line 10

   Source comment

   Below-two control by the tangent bound for the exponential.

   theorem scalar_rpow_lower (x δ : ℝ) (hx : 0 ≤ x) (hδ : 0 ≤ δ)
       (hp : 0 < 2 - δ) :
       x ^ 2 - δ * x ^ 2 * (x - 1) ≤ x ^ (2 - δ) := by
   …

2. theorem OAI.FourRow.normalized_entry_le line 27
3. theorem OAI.FourRow.cubic_sum_bound line 36
4. theorem OAI.FourRow.lpNorm_nonneg line 48
5. theorem OAI.FourRow.lpNorm_lower line 53
6. theorem OAI.FourRow.one_sub_sum_le_prod line 89
7. theorem OAI.FourRow.normalized_rowDist_le line 106
8. theorem OAI.FourRow.normalized_product_norm_lower line 112