OAI/Probability/SKGap/Localization/RefreshGenerator.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGapCutoff.refreshGenerator line 155
  2. def OAI.SKGapCutoff.refreshGradientGenerator line 158
  3. theorem OAI.SKGapCutoff.refreshHalfDiff_generator line 165
  4. def OAI.SKGapCutoff.refreshGeneratorLM line 181
  5. def OAI.SKGapCutoff.refreshGradientGeneratorLM line 197
  6. def OAI.SKGapCutoff.refreshGeneratorCLM line 226
  7. def OAI.SKGapCutoff.refreshGradientGeneratorCLM line 229
  8. def OAI.SKGapCutoff.refreshSemigroup line 233
  9. def OAI.SKGapCutoff.refreshGradientSemigroup line 236
  10. theorem OAI.SKGapCutoff.refreshHalfDiff_semigroup line 240
  11. theorem OAI.SKGapCutoff.refreshGenerator_const line 255
  12. theorem OAI.SKGapCutoff.refreshSemigroup_const line 259
  13. lemma OAI.SKGapCutoff.refreshGenerator_mul line 266
  14. lemma OAI.SKGapCutoff.refreshSemigroup_hasDerivAt line 276
  15. lemma OAI.SKGapCutoff.refreshSemigroup_hasDerivAt' line 281
  16. lemma OAI.SKGapCutoff.refreshSemigroup_apply_hasDerivAt line 286
  17. lemma OAI.SKGapCutoff.refreshSemigroup_apply_hasDerivAt' line 292
  18. lemma OAI.SKGapCutoff.refreshSemigroup_continuous line 298
  19. lemma OAI.SKGapCutoff.refreshSemigroup_zero line 304
  20. def OAI.SKGapCutoff.refreshJumpEnergy line 307
  21. lemma OAI.SKGapCutoff.refreshGenerator_square line 310
  22. lemma OAI.SKGapCutoff.refreshBackward_flow_hasDerivAt line 316
  23. lemma OAI.SKGapCutoff.refreshBackward_square_hasDerivAt line 323
  24. lemma OAI.SKGapCutoff.refreshInterpolated_square_hasDerivAt line 335
  25. lemma OAI.SKGapCutoff.refreshJumpEnergy_continuous line 352
  26. lemma OAI.SKGapCutoff.refreshInterpolated_energy_continuous line 357
  27. lemma OAI.SKGapCutoff.refreshSemigroup_variance_integral line 365
  28. def OAI.SKGapCutoff.refreshJumpWeight line 375
  29. def OAI.SKGapCutoff.refreshInfluence line 378
  30. def OAI.SKGapCutoff.refreshVectorDissipation line 381
  31. lemma OAI.SKGapCutoff.refreshGenerator_vectorSquare line 385
  32. lemma OAI.SKGapCutoff.refreshGradient_square_identity line 396
  33. lemma OAI.SKGapCutoff.refreshGradientSemigroup_apply_hasDerivAt line 416
  34. lemma OAI.SKGapCutoff.refreshBackward_gradient_hasDerivAt line 426
  35. lemma OAI.SKGapCutoff.refreshBackward_vectorSquare_hasDerivAt line 434
  36. def OAI.SKGapCutoff.refreshRoughDefect line 447
  37. lemma OAI.SKGapCutoff.refreshInterpolated_vectorSquare_hasDerivAt line 452
  38. lemma OAI.SKGapCutoff.refreshGeneratorCLM_eq line 476
  39. lemma OAI.SKGapCutoff.refreshSemigroup_uniformization line 483
  40. lemma OAI.SKGapCutoff.refreshSemigroup_nonneg line 490
  41. lemma OAI.SKGapCutoff.refreshJumpWeight_pos line 509
  42. lemma OAI.SKGapCutoff.refreshJumpWeight_le_two line 516
  43. lemma OAI.SKGapCutoff.refreshVectorDissipation_nonneg line 523
  44. lemma OAI.SKGapCutoff.refreshGradient_first_order_bound line 529
  45. lemma OAI.SKGapCutoff.refreshGradient_square_le line 566