OAI/Computability/MinUncut/Analysis/FreshCorrelation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MinUncut.Inner.spatialEnergy_eq_expect line 17
  2. lemma OAI.MinUncut.Inner.spatial_young line 21
  3. lemma OAI.MinUncut.Inner.gradient_correlation_truncate line 30
  4. lemma OAI.MinUncut.Inner.thirdRejection_measurable line 57
  5. lemma OAI.MinUncut.Inner.thirdRejection_nonneg line 74
  6. lemma OAI.MinUncut.Inner.thirdRejection_abs_le line 81
  7. lemma OAI.MinUncut.Inner.thirdRejection_integrable line 99
  8. lemma OAI.MinUncut.Inner.lowGradient_continuous line 104
  9. lemma OAI.MinUncut.Inner.lowGradient_correlation_continuous line 109
  10. lemma OAI.MinUncut.Inner.lowGradient_correlation_integrable line 118
  11. def OAI.MinUncut.Inner.averagedCorrelation line 131
  12. def OAI.MinUncut.Inner.thirdError line 134
  13. lemma OAI.MinUncut.Inner.lowGradient_inner_identity line 137
  14. lemma OAI.MinUncut.Inner.lowGradient_correlation_truncated line 165
  15. lemma OAI.MinUncut.Inner.lowGradient_correlation_truncated_weighted line 217