OAI/Dynamics/SmoothObstruction/PairLaw.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SmoothObstruction.PairLaw.cell line 16
  2. def OAI.SmoothObstruction.PairLaw.law line 21

    Source documentation

    The manuscript's original, unnormalized-on-retained-pairs law. All zero-mass cells contribute zero; no conditional renormalization is used.

    noncomputable def law (μ : Measure X) (P : X → α) : Measure (X × X) :=
…
  3. lemma OAI.SmoothObstruction.PairLaw.sum_cells line 24
  4. lemma OAI.SmoothObstruction.PairLaw.normalized_cell line 37
  5. lemma OAI.SmoothObstruction.PairLaw.first_marginal line 44
  6. lemma OAI.SmoothObstruction.PairLaw.second_marginal line 52
  7. theorem OAI.SmoothObstruction.PairLaw.law_probability line 60
  8. lemma OAI.SmoothObstruction.PairLaw.bad_pair_bound line 66
  9. structure OAI.SmoothObstruction.SwitchData line 90

    Source documentation

    A finite original cell-weighted pair law and its measurable switch. The carrier is not normalized and no sigma-algebra on the retained subtype is silently substituted for the ambient original pair law.

    structure SwitchData {M : Type} [MeasurableSpace M] (μ : Measure M) where
…
  10. def OAI.SmoothObstruction.SwitchData.law line 104
  11. def OAI.SmoothObstruction.SwitchData.retained line 105
  12. def OAI.SmoothObstruction.SwitchData.Good line 106
  13. def OAI.SmoothObstruction.SmoothSwitching line 113

    Source documentation

    The literal quantitative smooth switching property, with one fixed sequence of original finite cell laws, summable sixteenth powers, and uniform two-sided shadowing over the full dyadic windows.

    def SmoothSwitching {M : Type} [MetricSpace M] [MeasurableSpace M]
    (μ : Measure M) (S Sinv : M → M) : Prop :=
…