OAI/Analysis/CircleDomains/Probability/TagPaymentMeasure.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The local tag cost is an actual measure on parameter time: a weighted physical-length part plus one atom for each flagged visit.

  1. def OAI.CircleDomainRigidity.boundaryTimeMeasure line 16
  2. theorem OAI.CircleDomainRigidity.boundaryTimeMeasure_apply line 20
  3. theorem OAI.CircleDomainRigidity.boundaryTimeMeasure_univ line 26
  4. def OAI.CircleDomainRigidity.tagPaymentMeasure line 32
  5. theorem OAI.CircleDomainRigidity.tagPaymentMeasure_univ line 36
  6. theorem OAI.CircleDomainRigidity.tagPaymentMeasure_finite line 43
  7. theorem OAI.CircleDomainRigidity.tagPaymentMeasure_null_free line 51
  8. theorem OAI.CircleDomainRigidity.boundaryTimeMeasure_image_le line 66

    Source documentation

    Paying once at each distinct image point is bounded by paying at every visit.

    theorem boundaryTimeMeasure_image_le {X : Type*} (γ : PathTime → X) (m : X → ℝ≥0∞)
    {S : Set PathTime} (hS : MeasurableSet S) {A : Set X} (hA : A ⊆ γ '' S) :
    (∑' x : A, m x.val) ≤ boundaryTimeMeasure γ m S := by
…

    Mentions: OAI.CircleDomainRigidity.PathTime, OAI.CircleDomainRigidity.boundaryTimeMeasure