FrameIntersectionCosts.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Frame Intersection Costs

theorem OAI.HadwigerCounterexample.prod_one line 13
theorem OAI.HadwigerCounterexample.raw_part line 33
Source documentation
Raw law of a single-sign observation of primary/channel columns.
```
theorem raw_part (m : Mixer p n) (z : Place p) [DecidableEq I]
    (hN : 2*num (Full p n)-N≤ -1)
    {A : Mat (Full p n) I} (hA : Injective A.mulVec) :
    mapW (raw m N) (fun x => takeSign (p:=p) (x z.1) z.2 * A)=
…
```
Mentions: OAI.HadwigerCounterexample.Mixer, OAI.HadwigerCounterexample.Place, OAI.HadwigerCounterexample.num, OAI.HadwigerCounterexample.Full, OAI.HadwigerCounterexample.Mat, OAI.HadwigerCounterexample.mapW, OAI.HadwigerCounterexample.raw, OAI.HadwigerCounterexample.takeSign
def OAI.HadwigerCounterexample.ipPart line 52
theorem OAI.HadwigerCounterexample.frameP_cap line 55
theorem OAI.HadwigerCounterexample.frameY_cap line 79
theorem OAI.HadwigerCounterexample.any_span_hit line 103
def OAI.HadwigerCounterexample.expand line 126
theorem OAI.HadwigerCounterexample.transposed_uniform line 131
theorem OAI.HadwigerCounterexample.test_transpose line 139
Source documentation
per fixed nominal offsets in one component/side
```
theorem test_transpose {w : Wgt (UnitType p n N)} (m : Mixer p n) {H : ℝ} (hH : 0≤H)
    (h : bySide p w m H) (i : Bool) (z : Place p) (hN : 2*num (Full p n)-N≤ -1)
    (M : Mat (Fin N) I) (hM : Injective M.mulVec) :
    ∀ x,mapW w (fun y => (fyAt p (onSide y i) z)ᵀ * M) x≤H*2 * unif x := by
…
```
Mentions: OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.UnitType, OAI.HadwigerCounterexample.Mixer, OAI.HadwigerCounterexample.bySide, OAI.HadwigerCounterexample.Place, OAI.HadwigerCounterexample.num, OAI.HadwigerCounterexample.Full, OAI.HadwigerCounterexample.Mat, OAI.HadwigerCounterexample.mapW, OAI.HadwigerCounterexample.fyAt, OAI.HadwigerCounterexample.onSide, OAI.HadwigerCounterexample.unif
def OAI.HadwigerCounterexample.glimpsesBill line 153
theorem OAI.HadwigerCounterexample.glimpse_failure line 156
theorem OAI.HadwigerCounterexample.any_frame_hit line 184
Source documentation
span of entire individual primary image in a fixed cover mode.
```
theorem any_frame_hit {w : Wgt (UnitType p n N)} (m : Mixer p n) {H : ℝ} (hH : 0≤H)
    (h : bySide p w m H) (i : Bool) (z : Place p) (hN : 2*num (Full p n)-N≤ -1)
    (S : Space (Vec (Fin N))) :
    pr w (fun x => ¬ Disjoint (imageP p x i z) S) ≤
      H*2*bp (num (Row p n)+dim S-N) := by
…
```
Mentions: OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.UnitType, OAI.HadwigerCounterexample.Mixer, OAI.HadwigerCounterexample.bySide, OAI.HadwigerCounterexample.Place, OAI.HadwigerCounterexample.num, OAI.HadwigerCounterexample.Full, OAI.HadwigerCounterexample.Space, OAI.HadwigerCounterexample.Vec, OAI.HadwigerCounterexample.pr, OAI.HadwigerCounterexample.imageP, OAI.HadwigerCounterexample.bp, OAI.HadwigerCounterexample.Row, OAI.HadwigerCounterexample.dim