OAI/Combinatorics/HadwigerCounterexample/DerivativeCompression.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HadwigerCounterexample.mat_mul_fix line 13
2. theorem OAI.HadwigerCounterexample.compress_observer line 22

   Source documentation

   Endomorphism taking V into V, preserving dot product against S, of rank bounded by the observer space S.

   private theorem compress_observer (V S : Space (Vec I)) :
       ∃ A : Mat I I,(∀ v∈V,A *ᵥ v∈V) ∧
         (∀ v∈V,∀ y∈S, dotProduct y (A *ᵥ v) = dotProduct y v) ∧
         A.rank≤dim S := by
   …

   Mentions: OAI.HadwigerCounterexample.Space, OAI.HadwigerCounterexample.Vec, OAI.HadwigerCounterexample.Mat, OAI.HadwigerCounterexample.dim

3. def OAI.HadwigerCounterexample.priOut line 54
4. def OAI.HadwigerCounterexample.outSmall line 56
5. theorem OAI.HadwigerCounterexample.le_priOut line 59
6. theorem OAI.HadwigerCounterexample.dim_priOut line 62
7. theorem OAI.HadwigerCounterexample.outSmall_low line 67
8. theorem OAI.HadwigerCounterexample.ev_duom line 73
9. theorem OAI.HadwigerCounterexample.deriv_compress line 78
10. theorem OAI.HadwigerCounterexample.chanInner_pure line 129