OAI/Probability/SKFluctuations/LineDerivatives.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Line Derivatives.

  1. structure OAI.SKFluctuations.PinnedVariance.LineDerivatives line 23
  2. theorem OAI.SKFluctuations.PinnedVariance.convexOn_of_line_second_nonneg line 30
  3. def OAI.SKFluctuations.PinnedVariance.LineDerivatives.const_add line 56
  4. def OAI.SKFluctuations.PinnedVariance.LineDerivatives.quadraticPotential line 63
  5. theorem OAI.SKFluctuations.PinnedVariance.block_coercivity line 91
  6. theorem OAI.SKFluctuations.PinnedVariance.quadratic_remainder_lower_bound line 123
  7. theorem OAI.SKFluctuations.PinnedVariance.convexOn_quadraticPotential_slack line 153
  8. theorem OAI.SKFluctuations.PinnedVariance.variance_le_of_block_hessian line 202
  9. theorem OAI.SKFluctuations.PinnedVariance.block_nonneg_of_cauchySchwarz line 239
  10. theorem OAI.SKFluctuations.NoiseTransfer.real_fst_set line 258
  11. theorem OAI.SKFluctuations.NoiseTransfer.real_snd_set line 262
  12. theorem OAI.SKFluctuations.NoiseTransfer.interval_le_add_noise line 267
  13. theorem OAI.SKFluctuations.NoiseTransfer.tail_le_add_noise line 295
  14. theorem OAI.SKFluctuations.NoiseTransfer.strict_tail_le_variance line 326
  15. theorem OAI.SKFluctuations.NoiseTransfer.real_map_interval line 344
  16. theorem OAI.SKFluctuations.NoiseTransfer.real_map_absTail line 353
  17. theorem OAI.SKFluctuations.augmentedLaw_eq_completed line 366
  18. theorem OAI.SKFluctuations.completed_interval_bound line 374
  19. theorem OAI.SKFluctuations.completed_tail_bound line 386
  20. theorem OAI.SKFluctuations.freeEnergy_interval_bound line 400
  21. theorem OAI.SKFluctuations.freeEnergy_tail_bound line 422
  22. def OAI.SKFluctuations.Hierarchy.continuation line 451
  23. def OAI.SKFluctuations.Hierarchy.tiltedMean line 455
  24. theorem OAI.SKFluctuations.Hierarchy.source_lipschitz line 459
  25. theorem OAI.SKFluctuations.Hierarchy.exponential_local_bound line 471
  26. theorem OAI.SKFluctuations.Hierarchy.integrable_weighted line 484
  27. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_tested_integral line 494
  28. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_partition line 542
  29. theorem OAI.SKFluctuations.Hierarchy.partition_pos line 555
  30. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_continuation line 562
  31. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_tiltedMean line 583
  32. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_continuation_gradient line 617
  33. def OAI.SKFluctuations.Hierarchy.tiltedLaw line 633
  34. theorem OAI.SKFluctuations.Hierarchy.tiltedLaw_isProbability line 637
  35. theorem OAI.SKFluctuations.Hierarchy.integral_tiltedLaw line 642
  36. theorem OAI.SKFluctuations.Hierarchy.tiltedMean_nonneg line 654
  37. theorem OAI.SKFluctuations.Hierarchy.tiltedMean_square_sub_nonneg line 660