OAI/Combinatorics/IndependentSets/Reduction/SquareNorm.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.ProductAveraging.squareNorm line 9
  2. lemma OAI.LargeIndependentSets.ProductAveraging.squareNorm_eq_L2 line 11
  3. lemma OAI.LargeIndependentSets.ProductAveraging.squareNorm_sub_norm_le line 24
  4. lemma OAI.LargeIndependentSets.ProductAveraging.squareNorm_le_bound line 34
  5. def OAI.LargeIndependentSets.ProductAveraging.influenceNorm line 46
  6. lemma OAI.LargeIndependentSets.ProductAveraging.influenceNorm_difference line 48
  7. lemma OAI.LargeIndependentSets.ProductAveraging.influenceNorm_difference_le line 69
  8. lemma OAI.LargeIndependentSets.PhaseTest.quotient_dist_le line 81
  9. lemma OAI.LargeIndependentSets.PhaseTest.phase_measurable line 90
  10. lemma OAI.LargeIndependentSets.PhaseTest.phase_dist_le line 97
  11. lemma OAI.LargeIndependentSets.PhaseTest.phase_lipschitz line 116
  12. lemma OAI.LargeIndependentSets.PhaseTest.phase_change_coefficient line 123
  13. lemma OAI.LargeIndependentSets.PhaseTest.auxiliary_change_coefficient line 147
  14. lemma OAI.LargeIndependentSets.PhaseTest.auxiliary_influence_step line 159
  15. lemma OAI.LargeIndependentSets.PhaseTest.squared_value_distance line 177
  16. lemma OAI.LargeIndependentSets.PhaseTest.grid_square_error line 187