OAI/Analysis/NodalLength/WitnessPacking.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpNodal.Grid.sum_powers_le line 219
  2. lemma OAI.SharpNodal.Grid.sum_squared_powers_le line 229
  3. lemma OAI.SharpNodal.Grid.Cell.mem_mismatch_set line 234
  4. lemma OAI.SharpNodal.Grid.Cell.mismatch_set_subset line 240
  5. lemma OAI.SharpNodal.Grid.mismatch_at_scale line 245
  6. def OAI.SharpNodal.Grid.mismatchConstant line 291
  7. lemma OAI.SharpNodal.Grid.mismatch_for_larger line 293
  8. theorem OAI.SharpNodal.Grid.total_mismatch_bound line 334
  9. def OAI.SharpNodal.Grid.packingConstant line 362
  10. theorem OAI.SharpNodal.Grid.nearby_witness_packing line 366