AffineTimeSelection.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Synchronizing the shearing time windows

Affine changes of time with slope at least one half at most double Lebesgue measure. This yields the loss of eight in EKL (2006), Lemma 4.5. A finite family of bad windows can then be avoided simultaneously.

lemma OAI.DukePrimeDegree.volume_real_affine_preimage line 19
lemma OAI.DukePrimeDegree.affine_bad_time_bound line 27
lemma OAI.DukePrimeDegree.ekl_affine_time_mem line 45

theorem OAI.DukePrimeDegree.ekl_pullback_bad_time_bound line 52

Source documentation

The precise affine-time loss used to transfer the small-ball set from the interval of length 4*T to the shearing interval of length T.

theorem ekl_pullback_bad_time_bound (T θ η ε : ℝ)
    (hη : η = 0 ∨ η = 1) (E : Set ℝ) (hE : E ⊆ Ioc 0 (4 * T))
    (hbad : volume.real E ≤ ε * (4 * T)) :
    volume.real (Ioc 0 T ∩
      ((fun τ => (θ + (2 - η) * τ) / 2) ⁻¹' E)) ≤ 8 * ε * T := by
…

theorem OAI.DukePrimeDegree.exists_time_avoiding_finite_bad_sets line 71

Source documentation

Finite exceptional time sets whose relative losses sum to less than one leave a common admissible time.

theorem exists_time_avoiding_finite_bad_sets (m : ℕ) (T : ℝ) (hT : 0 < T)
    (B : Fin m → Set ℝ) (c : Fin m → ℝ)
    (hB : ∀ k, B k ⊆ Ioc 0 T)
    (hbad : ∀ k, volume.real (B k) ≤ c k * T)
    (hsum : ∑ k, c k < 1) :
    ∃ t ∈ Ioc 0 T, ∀ k, t ∉ B k := by
…