OAI/Analysis/CircleDomains/Probability/PhysicalOccupationPushforward.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Physical occupation is the pushforward of domain-time arclength, with parameter multiplicity retained. The value assigned at dust times is irrelevant.

  1. def OAI.CircleDomainRigidity.physicalValue line 19
  2. theorem OAI.CircleDomainRigidity.physicalValue_subpath line 22
  3. theorem OAI.CircleDomainRigidity.measurable_physicalValue line 31
  4. theorem OAI.CircleDomainRigidity.physicalDyadicLength_map line 37
  5. theorem OAI.CircleDomainRigidity.physicalStageTimeLength_map line 59
  6. theorem OAI.CircleDomainRigidity.physicalTimeLength_map line 72
  7. theorem OAI.CircleDomainRigidity.physicalOccupation_integral line 84