OAI/NumberTheory/Ostmann/Construction/OppositeBiasTransfer.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.residueTestMean line 12
2. theorem OAI.Ostmann.complementary_test_mean line 15
3. theorem OAI.Ostmann.paired_test_means line 27
4. theorem OAI.Ostmann.complementary_support_ratio line 37
5. theorem OAI.Ostmann.exists_opposite_bias_orientation line 49

   Source documentation

   The same orientation gives positive empirical bias on one side and negative empirical bias on the complementary side.

   theorem exists_opposite_bias_orientation (u v x y r δ : ℝ)
       (hδ : 0 < δ) (hr : 1 / 2 ≤ r) (hu : δ ≤ |u|) (hv : v = -r * u)
       (hx : |x - u| ≤ δ / 8) (hy : |y - v| ≤ δ / 8) :
       ∃ ε : ℝ, (ε = 1 ∨ ε = -1) ∧ δ / 4 ≤ ε * x ∧ δ / 4 ≤ -ε * y := by
   …

6. theorem OAI.Ostmann.complementary_empirical_bias line 75