OAI/Geometry/RCD/Heat/CompactHeatJointLaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual joint law of a heat-bridge point and its two endpoints

  1. def OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.jointDensity line 22
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.jointDensity_pos line 26
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.jointDensity_continuous line 35
  4. def OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.jointMeasure line 45
  5. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.jointMeasure_fst line 48
  6. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.jointMeasure_snd line 81
  7. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.jointMeasure_probability line 127
  8. def OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.jointLaw line 133