OAI/Analysis/FourierLLogL/Capture/Criterion.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Criteria and their polarized tests

  1. def OAI.FourierLLogL.Dyadic.Procedure.Capture.optic line 17
  2. def OAI.FourierLLogL.Dyadic.Procedure.Capture.energy line 18
  3. def OAI.FourierLLogL.Dyadic.Procedure.Capture.scalar line 19
  4. def OAI.FourierLLogL.Dyadic.Procedure.Capture.magnitude line 21
  5. def OAI.FourierLLogL.Dyadic.Procedure.Capture.strength line 24
  6. def OAI.FourierLLogL.Dyadic.Procedure.Capture.intense line 26
  7. def OAI.FourierLLogL.Dyadic.Procedure.Capture.amp line 29
  8. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.strength_bounds line 31
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.amp_pos line 36
  10. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.amp_hi line 39
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.gate_amp line 42
  12. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.intent_main line 45
  13. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.scalar_series line 49
  14. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.strong_sum line 57
  15. def OAI.FourierLLogL.Dyadic.Procedure.Capture.tracker line 65
  16. def OAI.FourierLLogL.Dyadic.Procedure.Capture.aim line 67
  17. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.aim_identity line 68
  18. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.criterion_bias line 102
  19. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.test_one line 120
  20. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.expensive_intent line 124
  21. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.edge_prob line 136
  22. theorem OAI.FourierLLogL.Dyadic.Procedure.Capture.masked_bias line 153

    Source documentation

    Mask of sufficient precision is a biased test under the post law

    theorem masked_bias {s : Scene M} {i : ℕ} (main : Bool) (x : Grid M)
    (hp : s.here.valid) (he : s.here.lev < M)
    (ha : 0 ≤ s.wage) (hn : 0 < s.norm) (hm : 0 < s.mass) (hM : s.mass ≤ 2*s.norm)
    (h : intense main s (side i) x)
    (hB : ¬ hazard s main i) (r : ℕ) (hr : side r ≤ amp i main /128) :
    ∃ g : Grid M → ℂ, (∀ z, ‖g z‖ ≤ 1) ∧ ∃ f : Grid M → ℝ,
      limitR f (band s.here i r) ∧ (∀ y, 0 ≤ f y ∧ f y ≤ 1) ∧
      expU (fun y => if y∈s.here.block M then 0 else f y) ≤ s.here.len*side r ∧
      amp i main /8 ≤ (tracker s main).Ex (fun y => f y.1*(g y.2*chi x y.1).re) := by
…

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.Procedure.Capture.intense, OAI.FourierLLogL.Dyadic.Procedure.hazard, OAI.FourierLLogL.Dyadic.Procedure.Capture.amp, OAI.FourierLLogL.Dyadic.Procedure.Capture.limitR, OAI.FourierLLogL.Dyadic.Procedure.Capture.band, OAI.FourierLLogL.Dyadic.expU, OAI.FourierLLogL.Dyadic.Procedure.Capture.tracker, OAI.FourierLLogL.Dyadic.chi