OAI/Computability/MinUncut/Estimates/InnerAssembly.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MinUncut.Average.weighted_sqrt_mul_sqrt line 11
  2. lemma OAI.MinUncut.Average.weighted_sqrt line 25
  3. lemma OAI.MinUncut.Average.expect_sqrt_mul_sqrt line 31
  4. lemma OAI.MinUncut.Inner.faceCorrelation_sum_le line 45
  5. lemma OAI.MinUncut.Inner.faceCorrelation_integrable line 53
  6. def OAI.MinUncut.Inner.classField line 67
  7. lemma OAI.MinUncut.Inner.classField_memLp line 72
  8. lemma OAI.MinUncut.Inner.classField_measurable line 78
  9. lemma OAI.MinUncut.Inner.classField_correlation_integrable line 84
  10. lemma OAI.MinUncut.Inner.lowGradient_class_partition line 91
  11. lemma OAI.MinUncut.Inner.lowGradient_classes_correlation line 97
  12. def OAI.MinUncut.RowNoise.jointL1 line 120
  13. lemma OAI.MinUncut.RowNoise.jointL1_le_sqrt line 123
  14. lemma OAI.MinUncut.Inner.averagedEnergy_eq_expect_joint line 136
  15. lemma OAI.MinUncut.Inner.retainedClass_localized line 144
  16. lemma OAI.MinUncut.Inner.class_localization_energy line 148
  17. lemma OAI.MinUncut.Inner.class_localization_l1 line 184
  18. lemma OAI.MinUncut.Slice.processed_average_integral_loss line 221
  19. def OAI.MinUncut.Inner.pairProcessed line 255
  20. lemma OAI.MinUncut.Inner.pairSlice_resample line 262
  21. lemma OAI.MinUncut.Inner.pair_processing_loss_law line 276
  22. lemma OAI.MinUncut.Inner.pairProcessed_measurable line 312
  23. lemma OAI.MinUncut.Inner.pairProcessed_memLp line 319
  24. lemma OAI.MinUncut.Inner.pairSlice_jointEnergy line 326
  25. lemma OAI.MinUncut.Inner.pair_processing_loss_integral line 337
  26. lemma OAI.MinUncut.Inner.pairSlice_atom_integral_law line 371
  27. lemma OAI.MinUncut.Inner.pairSlice_atom_integral_le line 383
  28. lemma OAI.MinUncut.Inner.retained_energy_le line 401
  29. lemma OAI.MinUncut.RowNoise.jointL1_sub_triangle line 416
  30. lemma OAI.MinUncut.Inner.pointedJointL1_bayes line 442
  31. lemma OAI.MinUncut.Inner.faceCorrelation_pointed_compare line 457
  32. lemma OAI.MinUncut.Inner.averagedCorrelation_pointed_compare line 473
  33. def OAI.MinUncut.Slice.lossBound line 522
  34. lemma OAI.MinUncut.Slice.lossBound_mono line 524
  35. lemma OAI.MinUncut.Slice.lossBound_expect line 529
  36. lemma OAI.MinUncut.Slice.lossBound_weighted line 538
  37. def OAI.MinUncut.Inner.pairAtomMean line 556
  38. lemma OAI.MinUncut.Inner.pairAtomMean_nonneg line 562
  39. lemma OAI.MinUncut.Inner.pairAtomMean_uniform_le line 567
  40. lemma OAI.MinUncut.Inner.pair_processing_loss_average line 583
  41. lemma OAI.MinUncut.RowNoise.oddAtom_le_bound line 629
  42. lemma OAI.MinUncut.RowNoise.measurable_oddAtom line 641
  43. def OAI.MinUncut.Inner.rowAtom line 665
  44. lemma OAI.MinUncut.Inner.rowAtom_nonneg line 669
  45. lemma OAI.MinUncut.Inner.rowAtom_le_gradientBound line 673
  46. lemma OAI.MinUncut.Inner.gradient_measurable line 678
  47. lemma OAI.MinUncut.Inner.rowAtom_measurable line 689
  48. lemma OAI.MinUncut.Inner.rowAtom_memLp line 694
  49. def OAI.MinUncut.Inner.rowAtomIndicator line 699
  50. lemma OAI.MinUncut.Inner.rowAtomIndicator_integrable line 703
  51. def OAI.MinUncut.Inner.rowEventProbability line 714
  52. def OAI.MinUncut.Inner.atomProbability line 717
  53. lemma OAI.MinUncut.Inner.rowEventProbability_nonneg line 720
  54. lemma OAI.MinUncut.Inner.rowAtom_sq_le line 726
  55. lemma OAI.MinUncut.Inner.rowAtom_secondMoment line 742
  56. lemma OAI.MinUncut.Inner.fixed_row_probability_le line 759