OAI/Computability/MinUncut/Estimates/EuclideanInvariantScore.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MinUncut.GaussianKernel.euclidean_invariant_score line 17
  2. lemma OAI.MinUncut.GaussianKernel.invariant_score line 42
  3. lemma OAI.MinUncut.GaussianKernel.coupled_score line 54
  4. lemma OAI.MinUncut.GaussianKernel.scalar_abs_mean_le_one line 108
  5. lemma OAI.MinUncut.GaussianKernel.bounded_scalar_score line 122
  6. lemma OAI.MinUncut.Inner.query_shift_cancel line 146
  7. lemma OAI.MinUncut.Inner.answer_coupled_shift line 164
  8. def OAI.MinUncut.Inner.tableCoefficient line 186
  9. theorem OAI.MinUncut.Inner.gradient_table_representation line 192
  10. lemma OAI.MinUncut.GaussianSmoothing.integral_split_other line 221
  11. def OAI.MinUncut.GaussianKernel.thresholdTable line 233
  12. lemma OAI.MinUncut.GaussianKernel.measurable_thresholdTable line 237
  13. def OAI.MinUncut.GaussianKernel.tableSensitivity line 248
  14. lemma OAI.MinUncut.GaussianKernel.measurable_tableSensitivity line 252
  15. lemma OAI.MinUncut.GaussianKernel.tableSensitivity_nonneg line 259
  16. lemma OAI.MinUncut.GaussianKernel.tableSensitivity_abs_le line 263
  17. lemma OAI.MinUncut.GaussianKernel.tableSensitivity_integrable line 266
  18. lemma OAI.MinUncut.GaussianKernel.forced_threshold_split line 272
  19. lemma OAI.MinUncut.GaussianKernel.tableSensitivity_split line 282
  20. lemma OAI.MinUncut.GaussianKernel.equal_forced_value line 289
  21. lemma OAI.MinUncut.GaussianKernel.conditional_table_score line 297
  22. theorem OAI.MinUncut.GaussianKernel.table_score_le line 313
  23. lemma OAI.MinUncut.Inner.bitSign_eq_iff line 347
  24. def OAI.MinUncut.Inner.thirdFailure line 350
  25. lemma OAI.MinUncut.Inner.thirdFailure_nonneg line 356
  26. lemma OAI.MinUncut.Inner.thirdFailure_abs_le line 361
  27. lemma OAI.MinUncut.Inner.measurable_thirdFailure line 366
  28. lemma OAI.MinUncut.Inner.query_eq_threshold line 378
  29. lemma OAI.MinUncut.Inner.thirdFailure_eq_sensitivity line 384
  30. lemma OAI.MinUncut.Inner.table_score_le_thirdFailure line 394
  31. lemma OAI.MinUncut.Inner.tableCoefficient_abs_le line 406
  32. def OAI.MinUncut.Inner.tableMass line 439
  33. def OAI.MinUncut.Inner.thirdRejection line 442
  34. theorem OAI.MinUncut.Inner.tableMass_le_thirdRejection line 446