OAI/Analysis/CircleDomains/Probability/PhysicalOccupationCost.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Weighted physical costs are integrals against the actual mean occupation. Square bounds on the density, differential and visit weights give the finite costs needed for the parameter-time payment measure.

  1. theorem OAI.CircleDomainRigidity.lintegral_physicalOccupationCode line 22
  2. theorem OAI.CircleDomainRigidity.lintegral_physical_cost_le_square_norms line 29
  3. theorem OAI.CircleDomainRigidity.ae_physical_cost_finite line 42
  4. theorem OAI.CircleDomainRigidity.ae_physical_and_visit_cost_finite line 57