OAI/Analysis/CircleDomains/Probability/PathLawMixtures.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Borel mixtures of actual path laws. Hit probabilities obey the mixture identity; their finite nonnegative weighted bounds pass to arbitrary probability mixtures. The dual finite bounds imply square summability and countable positive support.

  1. def OAI.CircleDomainRigidity.probabilityMixture line 21
  2. theorem OAI.CircleDomainRigidity.probabilityMixture_apply line 28
  3. def OAI.CircleDomainRigidity.pathHitReal line 40
  4. theorem OAI.CircleDomainRigidity.pathHitReal_nonneg line 44
  5. theorem OAI.CircleDomainRigidity.pathHitReal_le_one line 48
  6. theorem OAI.CircleDomainRigidity.measurable_pathHitProbability line 53
  7. theorem OAI.CircleDomainRigidity.integrable_pathHitReal line 58
  8. theorem OAI.CircleDomainRigidity.pathHitProbability_mixture line 68
  9. theorem OAI.CircleDomainRigidity.pathHitReal_mixture line 74
  10. def OAI.CircleDomainRigidity.HasHitNormBound line 84

    Source documentation

    The finite nonnegative dual tests for the square norm of the hit vector.

    def HasHitNormBound (μ : ProbabilityMeasure C(PathTime, X)) (C : ℝ) : Prop :=
…

    Mentions: OAI.CircleDomainRigidity.PathTime

  11. theorem OAI.CircleDomainRigidity.HasHitNormBound.mixture line 88
  12. theorem OAI.CircleDomainRigidity.HasHitNormBound.sum_sq_le line 106
  13. theorem OAI.CircleDomainRigidity.HasHitNormBound.summable_sq line 118
  14. theorem OAI.CircleDomainRigidity.HasHitNormBound.countable_positive_support line 124