OAI/Probability/SLE/Gauge/BatchEntryOrder.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SLEExactGauge.Target.prefix_eq_sum line 15
2. lemma OAI.SLEExactGauge.Target.prefix_add_le line 27
3. lemma OAI.SLEExactGauge.Target.entryPosition_strict_of_key_lt line 46
4. lemma OAI.SLEExactGauge.Target.entryPosition_injective_on_batch line 56
5. lemma OAI.SLEExactGauge.Target.entryRadius_lt_of_position_lt line 69
6. theorem OAI.SLEExactGauge.Target.ordered_repeated_batch line 83

   Source documentation

   The repeated tests have a finite chronological enumeration, without discarding entries whose dyadic thresholds coincide.

   theorem ordered_repeated_batch (κ : ℝ) (W : WienerLaw) {n : ℕ}
       (hn : 1 ≤ n) (hm1 : 0 < moment κ W 1)
       (hJ : moment κ W 1^n ≤ moment κ W n) :
       ∃ (J : ℕ) (e : Fin J → ℤ × ℕ),
         Function.Injective e ∧
         (∀ kj, kj ∈ Set.range e ↔ kj.2 < multiplicity κ W n kj.1) ∧
         StrictMono (fun i => entryPosition κ W (n,some (e i))) := by
   …

   Mentions: OAI.SLEExactGauge.Target.WienerLaw, OAI.SLEExactGauge.Target.moment, OAI.SLEExactGauge.Target.multiplicity, OAI.SLEExactGauge.Target.entryPosition