OAI/Combinatorics/Permanent/Perturbation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FourRow.abs_mul_le_half_sq line 10

   Source comment

   Exact marginal cancellation controls all perturbations quadratically.

   theorem abs_mul_le_half_sq (a b : ℝ) : |a * b| ≤ (a ^ 2 + b ^ 2) / 2 := by
   …

2. theorem OAI.FourRow.pair_shift_sq_le line 16
3. theorem OAI.FourRow.product_remainder_bound line 23
4. theorem OAI.FourRow.uniform_probability line 50
5. theorem OAI.FourRow.uniform_marginals line 55
6. theorem OAI.FourRow.marginal_average line 61
7. theorem OAI.FourRow.law_linear_expectation line 71
8. theorem OAI.FourRow.normalized_perturbation line 79