OAI/Analysis/FourierLLogL/Snapshot/Display.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.rangeIx line 14
2. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.precision line 15
3. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.sharp line 16
4. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.portrait line 17
5. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.distance line 20
6. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.sharp_pos line 22
7. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.coordinate_le line 24
8. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.image_income line 38
9. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.portrait_compare line 49
10. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.close_display line 64

    Source documentation

    Scenes with close portrait. No equality of scene or area needed.

    lemma close_display (s t : Scene M) (b : Bool) (d : Finset (Grid M)) (i m : ℕ) (hd : d.card ≤ rangeIx m)
        (p : Grid M) (he : enclosed d 1 p) (hh : distance (portrait b s d i m) (portrait b t d i m) ≤ sharp i)
        (hs : ReadyAt s) (ht : ReadyAt t) (ha : 0 ≤ s.norm) (hb : 0 ≤ t.norm)
        (hc : share s ≤ 4) (hC : share t ≤ 4) :
        magnitude b s p ≤ magnitude b t p +20*sharp i := by
    …

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.Procedure.Snapshot.rangeIx, OAI.FourierLLogL.Dyadic.enclosed, OAI.FourierLLogL.Dyadic.Procedure.Snapshot.distance, OAI.FourierLLogL.Dyadic.Procedure.Snapshot.portrait, OAI.FourierLLogL.Dyadic.Procedure.Snapshot.sharp, OAI.FourierLLogL.Dyadic.Procedure.share