FrameOrbitLaws.lean`

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Frame Orbit Laws

def OAI.HadwigerCounterexample.FramesAt line 14
structure OAI.HadwigerCounterexample.Move line 17
def OAI.HadwigerCounterexample.Move.sym line 25
def OAI.HadwigerCounterexample.Move.dual line 26
def OAI.HadwigerCounterexample.Move.permMat line 28
def OAI.HadwigerCounterexample.Move.perm line 33
theorem OAI.HadwigerCounterexample.Move.gram_invar line 37
theorem OAI.HadwigerCounterexample.Move.L_inj line 42
theorem OAI.HadwigerCounterexample.Move.perm_inj line 48
theorem OAI.HadwigerCounterexample.Move.invar line 54
theorem OAI.HadwigerCounterexample.framesAt_exists line 63
Source documentation
Nonempty matrix family if super-dimension slack.
```
theorem framesAt_exists [DecidableEq I] [DecidableEq J]
    {C : Mat I J → Prop} (h : ∃ G, C G) (hn : num I+num J < num U) :
    ∃ x : Mat U I × Mat U J, FramesAt C x := by
…
```
Mentions: OAI.HadwigerCounterexample.Mat, OAI.HadwigerCounterexample.num, OAI.HadwigerCounterexample.FramesAt
theorem OAI.HadwigerCounterexample.move_exists line 79
theorem OAI.HadwigerCounterexample.move_exists_one line 84
def OAI.HadwigerCounterexample.observe line 95
theorem OAI.HadwigerCounterexample.framesAt_observe line 99
Source documentation
Uniform law of sub-batch with Gram fixed on the batch.
```
theorem framesAt_observe {C : Mat I J → Prop} (hc : ∃ x : Mat U I × Mat U J, FramesAt C x)
    (P : Mat I R) (Q : Mat J S) {G : Mat R S} (hP : Injective P.mulVec)
    (hQ : Injective Q.mulVec) (h : ∀ M, C M → Pᵀ*M*Q=G) :
    mapW (unifOn (FramesAt (U:=U) C)) (observe P Q) = unifOn (gramGood G) := by
…
```
Mentions: OAI.HadwigerCounterexample.Mat, OAI.HadwigerCounterexample.FramesAt, OAI.HadwigerCounterexample.mapW, OAI.HadwigerCounterexample.unifOn, OAI.HadwigerCounterexample.observe, OAI.HadwigerCounterexample.gramGood
theorem OAI.HadwigerCounterexample.framesAt_observe_plus line 119
Source documentation
Uniform law of plus-only observation; in particular plus frames are uniform injective.
```
theorem framesAt_observe_plus {C : Mat I J → Prop} (hc : ∃ x : Mat U I × Mat U J, FramesAt C x)
    {P : Mat I R} (hP : Injective P.mulVec) :
    mapW (unifOn (FramesAt (U:=U) C)) (fun x => x.1*P) =
…
```
Mentions: OAI.HadwigerCounterexample.Mat, OAI.HadwigerCounterexample.FramesAt, OAI.HadwigerCounterexample.mapW, OAI.HadwigerCounterexample.unifOn
theorem OAI.HadwigerCounterexample.framesAt_observe_minus line 132
theorem OAI.HadwigerCounterexample.plus_marginal line 145