OAI/Probability/SKFluctuations/UniformGridConvergence.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

Uniform Grid Convergence.

  1. theorem OAI.SKFluctuations.Hierarchy.HeatJet.uniform_grid_convergence line 19
  2. theorem OAI.SKFluctuations.Hierarchy.HeatJet.continuous_nonnegativeProfileValue line 35
  3. def OAI.SKFluctuations.Hierarchy.boundedMassProfiles line 49
  4. theorem OAI.SKFluctuations.Hierarchy.boundedMassProfiles_compact line 52
  5. def OAI.SKFluctuations.Hierarchy.boundedNonnegativeProfile line 56
  6. theorem OAI.SKFluctuations.Hierarchy.continuous_boundedProfile_value line 61
  7. def OAI.SKFluctuations.Hierarchy.dyadicLowerSum line 75
  8. theorem OAI.SKFluctuations.Hierarchy.dyadicLowerSum_continuous line 79
  9. theorem OAI.SKFluctuations.Hierarchy.dyadicLowerSum_integral_bounds line 87
  10. theorem OAI.SKFluctuations.Hierarchy.dyadicLowerSum_integral_error line 121
  11. def OAI.SKFluctuations.Hierarchy.scalarFeature line 138
  12. def OAI.SKFluctuations.Hierarchy.scalarTerminal line 141
  13. theorem OAI.SKFluctuations.Hierarchy.scalarTerminal_F line 146
  14. theorem OAI.SKFluctuations.Hierarchy.scalarTerminal_G_bound line 156
  15. def OAI.SKFluctuations.Hierarchy.weightedProfile line 182
  16. theorem OAI.SKFluctuations.Hierarchy.weightedProfile_monotone line 184
  17. def OAI.SKFluctuations.Hierarchy.scalarPenalty line 187
  18. theorem OAI.SKFluctuations.Hierarchy.scalarPenalty_eq line 189
  19. theorem OAI.SKFluctuations.Hierarchy.scalarPenalty_continuous line 197
  20. def OAI.SKFluctuations.Hierarchy.scalarProfiles line 226
  21. theorem OAI.SKFluctuations.Hierarchy.scalarProfiles_closed line 229
  22. theorem OAI.SKFluctuations.Hierarchy.scalarProfiles_nonempty line 246
  23. def OAI.SKFluctuations.Hierarchy.rescaledMassProfile line 263
  24. def OAI.SKFluctuations.Hierarchy.scalarParisiValue line 270
  25. theorem OAI.SKFluctuations.Hierarchy.scalarParisiValue_continuous line 274
  26. theorem OAI.SKFluctuations.Hierarchy.scalarParisiValue_attains_minimum line 282
  27. theorem OAI.SKFluctuations.Hierarchy.dyadicLowerSum_integral_error_control line 296
  28. theorem OAI.SKFluctuations.Hierarchy.monotone_abs_sub_error line 331
  29. theorem OAI.SKFluctuations.Hierarchy.PositiveMassProfile.pairedGrid_cost_eq_sum line 356
  30. theorem OAI.SKFluctuations.Hierarchy.monotone_abs_sub_sum_tendsto line 364
  31. theorem OAI.SKFluctuations.Hierarchy.HeatJet.profileValue_L1_comparison line 383
  32. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileValue_L1_comparison line 396
  33. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileValue_congr_ae line 407
  34. def OAI.SKFluctuations.Hierarchy.rightMassProfile line 428
  35. theorem OAI.SKFluctuations.Hierarchy.rightMassProfile_ae line 433
  36. theorem OAI.SKFluctuations.Hierarchy.rightMassProfile_mem line 441
  37. def OAI.SKFluctuations.Hierarchy.profileStieltjes line 451
  38. theorem OAI.SKFluctuations.Hierarchy.scalarProfile_tendsto_bot line 456
  39. theorem OAI.SKFluctuations.Hierarchy.scalarProfile_tendsto_top line 462
  40. theorem OAI.SKFluctuations.Hierarchy.profileStieltjes_probability line 468
  41. theorem OAI.SKFluctuations.Hierarchy.cdf_profileStieltjes line 475
  42. theorem OAI.SKFluctuations.Hierarchy.scalarParisiValue_congr_ae line 480
  43. theorem OAI.SKFluctuations.Hierarchy.scalarParisiValue_attains_distribution line 498
  44. theorem OAI.SKFluctuations.Hierarchy.profileStieltjes_left_zero line 523
  45. theorem OAI.SKFluctuations.Hierarchy.profileStieltjes_one line 530
  46. theorem OAI.SKFluctuations.Hierarchy.profileStieltjes_carried line 540
  47. theorem OAI.SKFluctuations.Hierarchy.profileStieltjes_Icc line 552
  48. theorem OAI.SKFluctuations.Hierarchy.HeatJet.grid_constant line 565
  49. theorem OAI.SKFluctuations.Hierarchy.HeatJet.profileValue_constant line 593
  50. theorem OAI.SKFluctuations.Hierarchy.HeatJet.grid_step line 613
  51. theorem OAI.SKFluctuations.Hierarchy.HeatJet.profileValue_step line 666