OAI/Analysis/FiniteFactor/CrossedProduct/AngleLaw.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceAngleUnit line 13

   Source documentation

   The source angle interval has length 1/N_s, where N_s=m_s K_s.

   def sourceAngleUnit (i : SourceCoordinate) : ℝ :=
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate

2. theorem OAI.FiniteFactor.sourceAngleUnit_pos line 16
3. def OAI.FiniteFactor.sourceAngleInterval line 19
4. def OAI.FiniteFactor.sourceAngleMarginal line 23

   Source documentation

   Normalized Lebesgue measure on the actual source interval.

   def sourceAngleMarginal (i : SourceCoordinate) : Measure ℝ :=
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate

5. theorem OAI.FiniteFactor.sourceAngleInterval_volume line 26
6. instance OAI.FiniteFactor.sourceAngleMarginal_probability line 30
7. instance OAI.FiniteFactor.sourceAngleMarginal_atomless line 37
8. def OAI.FiniteFactor.sourceAngleLaw line 44

   Source documentation

   This law is selected before any invariant projection is considered.

   def sourceAngleLaw : Measure (SourceCoordinate → ℝ) :=
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate

9. instance OAI.FiniteFactor.sourceAngleLaw_probability line 47
10. theorem OAI.FiniteFactor.sourceAngleLaw_coordinate line 51
11. theorem OAI.FiniteFactor.sourceAngleLaw_independent line 55
12. theorem OAI.FiniteFactor.sourceAngleLaw_cylinder line 59
13. theorem OAI.FiniteFactor.sourceAngleMarginal_ae line 65
14. theorem OAI.FiniteFactor.sourceAngleLaw_admissible line 70

    Source documentation

    All interval constraints hold simultaneously, not just coordinatewise.

    theorem sourceAngleLaw_admissible : ∀ᵐ θ ∂sourceAngleLaw, SourceAngles θ := by
    …

    Mentions: OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.SourceAngles

15. theorem OAI.FiniteFactor.sourceAngleLaw_operator line 81