OAI/Probability/SKFluctuations/InverseControlMeasureCalculus.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Inverse Control Measure Calculus.

  1. theorem OAI.SKFluctuations.Hierarchy.control_measures_finite line 15
  2. theorem OAI.SKFluctuations.Hierarchy.integral_controlPlus line 36
  3. theorem OAI.SKFluctuations.Hierarchy.integral_controlMinus line 49
  4. theorem OAI.SKFluctuations.Hierarchy.control_measures_nonzero line 71
  5. theorem OAI.SKFluctuations.Hierarchy.countable_nonzero_deriv_level line 131
  6. theorem OAI.SKFluctuations.Hierarchy.ae_deriv_zero_on_level line 149
  7. theorem OAI.SKFluctuations.Hierarchy.ae_contact_gradient_zero line 155
  8. def OAI.SKFluctuations.Hierarchy.controlPrimitiveExtension line 174
  9. theorem OAI.SKFluctuations.Hierarchy.controlPrimitiveExtension_on line 177
  10. theorem OAI.SKFluctuations.Hierarchy.controlPrimitiveExtension_continuous line 182
  11. theorem OAI.SKFluctuations.Hierarchy.controlPrimitiveExtension_integrable line 189
  12. theorem OAI.SKFluctuations.Hierarchy.control_gradient_potential line 198
  13. def OAI.SKFluctuations.Hierarchy.controlFactorExtension line 265
  14. theorem OAI.SKFluctuations.Hierarchy.controlFactorExtension_pos line 268
  15. theorem OAI.SKFluctuations.Hierarchy.controlFactorExtension_on line 271
  16. theorem OAI.SKFluctuations.Hierarchy.controlFactorExtension_continuous line 276
  17. theorem OAI.SKFluctuations.Hierarchy.control_density_bounds line 280
  18. theorem OAI.SKFluctuations.Hierarchy.control_cost_identity line 305
  19. theorem OAI.SKFluctuations.Hierarchy.integral_primitive_product line 352
  20. theorem OAI.SKFluctuations.Hierarchy.inverse_control_cost line 377
  21. theorem OAI.SKFluctuations.Hierarchy.control_first_variation_to_potential line 401
  22. def OAI.SKFluctuations.Hierarchy.inverseControlWeight line 546
  23. theorem OAI.SKFluctuations.Hierarchy.inverseControlWeight_mem line 549
  24. theorem OAI.SKFluctuations.Hierarchy.inverseControlWeight_measurable line 554
  25. theorem OAI.SKFluctuations.Hierarchy.inverseControlWeight_equation line 561
  26. theorem OAI.SKFluctuations.Hierarchy.inverseControlWeight_ae_equation line 571
  27. theorem OAI.SKFluctuations.source_minimum_potential line 590