ChannelFactorization.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Channel Factorization

theorem OAI.HadwigerCounterexample.biorth_exists line 15
Source documentation
Pairing rank after imposing orthogonality constraints.
```
theorem biorth_exists (S T : Space (Vec I)) (r : ℕ)
    (h : r+dim S+dim T≤Fintype.card I) :
    ∃ A B : Mat I (Fin r), colSp A≤ annih S ∧ colSp B≤ annih T ∧ Aᵀ*B=1 := by
…
```
Mentions: OAI.HadwigerCounterexample.Space, OAI.HadwigerCounterexample.Vec, OAI.HadwigerCounterexample.dim, OAI.HadwigerCounterexample.Mat, OAI.HadwigerCounterexample.colSp, OAI.HadwigerCounterexample.annih
theorem OAI.HadwigerCounterexample.pure_chan_split line 55
Source documentation
split desired respective bounded-rank bilinear form
```
theorem pure_chan_split (M : Mat J J) (S T : Space (Vec I)) (X Y : Space (Vec J))
    (h : M∈box (annih X) (annih Y)) (ht : M.rank+dim S+dim T ≤ Fintype.card I) :
    ∃ A ∈ box (annih S) (annih X),∃ B∈box (annih T) (annih Y), Aᵀ * B=M := by
…
```
Mentions: OAI.HadwigerCounterexample.Mat, OAI.HadwigerCounterexample.Space, OAI.HadwigerCounterexample.Vec, OAI.HadwigerCounterexample.box, OAI.HadwigerCounterexample.annih, OAI.HadwigerCounterexample.dim
theorem OAI.HadwigerCounterexample.chan_factor line 86
Source documentation
The final channel change for fixed B endpoint.
```
theorem chan_factor {f b : Plan p n} {P : PureForms p n} {C : ChanOut p n} {j : Bool}
    (H T K : ℕ) (hc : outSmall H C) (hK : ∀ z,dim (hPin b z j)≤K)
    (hh : T+2*(K+2*H)≤p.h)
    (hP : P∈pureSpace p f) (ht : ∀ e,(P e).rank≤T) :
    ∃ D∈deltaSpace p f b j,obsPair p (chanInner p (C+D) (C+D))=
      obsPair p (chanInner p C C)+obsPair p P := by
…
```
Mentions: OAI.HadwigerCounterexample.Plan, OAI.HadwigerCounterexample.PureForms, OAI.HadwigerCounterexample.ChanOut, OAI.HadwigerCounterexample.outSmall, OAI.HadwigerCounterexample.dim, OAI.HadwigerCounterexample.hPin, OAI.HadwigerCounterexample.pureSpace, OAI.HadwigerCounterexample.deltaSpace, OAI.HadwigerCounterexample.obsPair, OAI.HadwigerCounterexample.chanInner