OAI/Combinatorics/HadwigerCounterexample/IndependentPhaseBounds.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HadwigerCounterexample.PhasePair line 15
2. abbrev OAI.HadwigerCounterexample.Party line 16
3. def OAI.HadwigerCounterexample.uPhase line 18
4. def OAI.HadwigerCounterexample.joinPhase line 21
5. def OAI.HadwigerCounterexample.listens line 25

   Source documentation

   Read the whole channel frames of a unit.

   def listens (p : Shape) {n N} (x : UnitType p n N) : PhasePair p N :=
   …

   Mentions: OAI.HadwigerCounterexample.Shape, OAI.HadwigerCounterexample.UnitType, OAI.HadwigerCounterexample.PhasePair

6. def OAI.HadwigerCounterexample.tone line 28
7. def OAI.HadwigerCounterexample.pitch line 31
8. theorem OAI.HadwigerCounterexample.phase_actual line 36
9. theorem OAI.HadwigerCounterexample.perm_pair line 42
10. theorem OAI.HadwigerCounterexample.iid_prodM line 52
11. theorem OAI.HadwigerCounterexample.wsign_sum line 82
12. theorem OAI.HadwigerCounterexample.lawH_law line 89
13. theorem OAI.HadwigerCounterexample.lawH_phased line 92
14. def OAI.HadwigerCounterexample.freeH line 111
15. theorem OAI.HadwigerCounterexample.freeH_law line 113
16. theorem OAI.HadwigerCounterexample.free_phase line 117
17. theorem OAI.HadwigerCounterexample.phase_cap line 150

    Source documentation

    cap for channel cube pair from joint raw

    theorem phase_cap {w : Wgt (UnitType p n N)} {c : ℝ} (hc : 0≤c)
        (m : Mixer p n)
        (h : ∀ x,w x≤c*pairW (raw m N) (raw m N) x)
        (hN : 2*num (Full p n)-N≤ -1) (y : PhasePair p N) :
        mapW w (listens p) y≤c*chanPrice p^2 * freeH p N y := by
    …

    Mentions: OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.UnitType, OAI.HadwigerCounterexample.Mixer, OAI.HadwigerCounterexample.pairW, OAI.HadwigerCounterexample.raw, OAI.HadwigerCounterexample.num, OAI.HadwigerCounterexample.Full, OAI.HadwigerCounterexample.PhasePair, OAI.HadwigerCounterexample.mapW, OAI.HadwigerCounterexample.listens, OAI.HadwigerCounterexample.chanPrice, OAI.HadwigerCounterexample.freeH