OAI/Analysis/FiniteFactor/Coupling/TaggedAdmissibility.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.CouplingParameters.currentBoundary line 12
2. def OAI.FiniteFactor.CouplingParameters.currentTag line 15
3. def OAI.FiniteFactor.CouplingParameters.currentNonTag line 18
4. theorem OAI.FiniteFactor.CouplingParameters.currentBoundary_measurable line 21
5. theorem OAI.FiniteFactor.CouplingParameters.currentTag_measurable line 25
6. theorem OAI.FiniteFactor.CouplingParameters.currentNonTag_measurable line 28
7. theorem OAI.FiniteFactor.CouplingParameters.currentTag_mass line 31
8. theorem OAI.FiniteFactor.CouplingParameters.currentTag_disjoint line 48
9. theorem OAI.FiniteFactor.CouplingParameters.currentNonTag_mass_lower line 55

   Source documentation

   The source's one-coordinate nontagged admissible mass, including both endpoint losses, under the actual labelled coupling.

   theorem currentNonTag_mass_lower (p : CouplingParameters) :
       ENNReal.ofReal (1-41/p.m) ≤ p.labelledCoupling p.currentNonTag := by
   …

   Mentions: OAI.FiniteFactor.CouplingParameters