OAI/Probability/SKSupport/Support/Closure.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ZeroTemperatureSK.SupportDeterministic.Time line 11
  2. structure OAI.ZeroTemperatureSK.SupportDeterministic.IsOrderParameter line 13
  3. def OAI.ZeroTemperatureSK.SupportDeterministic.IsStieltjesMeasure line 19
  4. lemma OAI.ZeroTemperatureSK.SupportDeterministic.IsStieltjesMeasure.cdf_add_Ioc line 26
  5. lemma OAI.ZeroTemperatureSK.SupportDeterministic.IsStieltjesMeasure.eq_cdf_of_measure_Ioc_zero line 31
  6. lemma OAI.ZeroTemperatureSK.SupportDeterministic.IsStieltjesMeasure.measure_zero_of_disjoint_support line 38
  7. lemma OAI.ZeroTemperatureSK.SupportDeterministic.IsStieltjesMeasure.eq_cdf_of_support_free line 42
  8. lemma OAI.ZeroTemperatureSK.SupportDeterministic.IsStieltjesMeasure.lt_cdf_of_full_support line 47
  9. lemma OAI.ZeroTemperatureSK.SupportDeterministic.IsStieltjesMeasure.strictMonoOn_of_full_support line 64
  10. def OAI.ZeroTemperatureSK.SupportDeterministic.InSupport line 71
  11. lemma OAI.ZeroTemperatureSK.SupportDeterministic.inSupport_coe line 74
  12. lemma OAI.ZeroTemperatureSK.SupportDeterministic.exists_support_gap line 80
  13. lemma OAI.ZeroTemperatureSK.SupportDeterministic.support_cofinal_of_no_terminal_plateau line 123
  14. lemma OAI.ZeroTemperatureSK.SupportDeterministic.constant_on_support_gap line 148
  15. lemma OAI.ZeroTemperatureSK.SupportDeterministic.zero_on_initial_support_gap line 169
  16. lemma OAI.ZeroTemperatureSK.SupportDeterministic.IsStieltjesMeasure.finiteOnCompacts line 187
  17. lemma OAI.ZeroTemperatureSK.SupportDeterministic.isCompact_time_Iic line 199
  18. lemma OAI.ZeroTemperatureSK.SupportDeterministic.Variation.continuous_zero_on_support_of_integral_nonpos line 214
  19. theorem OAI.ZeroTemperatureSK.SupportDeterministic.Variation.zero_on_support_of_compact_mass_removal line 230
  20. lemma OAI.ZeroTemperatureSK.SupportDeterministic.Variation.value_contact_of_potential_min line 252
  21. lemma OAI.ZeroTemperatureSK.SupportDeterministic.Variation.derivative_contact_of_potential_min line 262
  22. theorem OAI.ZeroTemperatureSK.SupportDeterministic.Variation.contact_conditions line 295
  23. def OAI.ZeroTemperatureSK.SupportDeterministic.Variation.contactPotential line 315
  24. lemma OAI.ZeroTemperatureSK.SupportDeterministic.Variation.contact_integrable line 318
  25. lemma OAI.ZeroTemperatureSK.SupportDeterministic.Variation.contactPotential_continuousOn line 331
  26. lemma OAI.ZeroTemperatureSK.SupportDeterministic.Variation.contactPotential_hasDerivAt line 340
  27. theorem OAI.ZeroTemperatureSK.SupportDeterministic.Variation.no_gap_of_derivative_lt_one line 361
  28. theorem OAI.ZeroTemperatureSK.SupportDeterministic.Variation.no_gap_of_strictConvex_derivative line 370
  29. theorem OAI.ZeroTemperatureSK.SupportDeterministic.Variation.no_positive_constant_gap line 382
  30. theorem OAI.ZeroTemperatureSK.SupportDeterministic.Variation.no_zero_constant_gap line 393
  31. theorem OAI.ZeroTemperatureSK.SupportDeterministic.Variation.full_support_of_contact_and_gap_curvature line 411
  32. theorem OAI.ZeroTemperatureSK.SupportDeterministic.Variation.derivative_eq_one_of_full_contact line 462