OAI/Probability/ParisiFinite/WeightedGradientField.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Weighted Gradient Field.

  1. def OAI.ParisiFinite.ThirdJet.weightedGradientField line 19
  2. def OAI.ParisiFinite.ThirdJet.slabWeightedGradientTest line 45
  3. structure OAI.ParisiFinite.ScheduleWeightedGradient line 83
  4. def OAI.ParisiFinite.scheduleWeightedGradient line 94
  5. def OAI.ParisiFinite.finiteWeightedKernel line 145
  6. lemma OAI.ParisiFinite.finiteWeightedKernel_bound line 153
  7. lemma OAI.ParisiFinite.finiteWeightedKernel_integrable line 180
  8. lemma OAI.ParisiFinite.expected_finiteWeightedKernel_eq line 199
  9. lemma OAI.ParisiFinite.expected_finiteWeightedKernel_aestronglyMeasurable line 216
  10. lemma OAI.ParisiFinite.expected_finiteWeightedKernel_bound line 230
  11. theorem OAI.ParisiFinite.finite_schedule_weighted_verification line 239
  12. def OAI.ParisiFinite.weightedKernel line 278
  13. lemma OAI.ParisiFinite.global_dyadic_weightedKernel_tendsto line 285
  14. lemma OAI.ParisiFinite.expected_global_dyadic_weightedKernel_tendsto line 300
  15. lemma OAI.ParisiFinite.expected_global_dyadic_gradient_weighted_tendsto line 316
  16. theorem OAI.ParisiFinite.canonical_weighted_verification line 344
  17. def OAI.ParisiFinite.sineWeight line 403
  18. lemma OAI.ParisiFinite.sineWeight_bound line 420
  19. lemma OAI.ParisiFinite.sineWeight_zero line 426
  20. lemma OAI.ParisiFinite.sineWeight_bound_abs line 427
  21. lemma OAI.ParisiFinite.sineWeight_tendsto line 432
  22. lemma OAI.ParisiFinite.sineWeight_d1_tendsto line 449
  23. lemma OAI.ParisiFinite.sineWeight_d2_tendsto line 457
  24. lemma OAI.ParisiFinite.sineWeight_bound2_le line 467
  25. lemma OAI.ParisiFinite.expected_weightedKernel_aestronglyMeasurable line 485
  26. def OAI.ParisiFinite.BoundedCoefficient.weightedFeedback line 503
  27. lemma OAI.ParisiFinite.BoundedCoefficient.weightedKernel_feedback line 508
  28. lemma OAI.ParisiFinite.BoundedCoefficient.weightedFeedback_bound line 513
  29. lemma OAI.ParisiFinite.BoundedCoefficient.weightedFeedback_integrable line 541
  30. lemma OAI.ParisiFinite.BoundedCoefficient.expected_feedback_sine_tendsto line 556
  31. theorem OAI.ParisiFinite.BoundedCoefficient.position_spin_raw line 578