The threshold test of Section 5

This file proves the claim of Section 5 of the paper that the test that rejects the null as soon as the conditional e-variables E*_t = ∏_{i=2}^t ℓ(Y_i) reach 1/α has level α, following the paper: these e-variables form a test martingale with respect to the filtration (𝒢_t) generated by the variables Y_i (Proposition 2), and Ville's inequality in this filtration bounds the probability that they ever reach 1/α by α under every null distribution.

• isTestSupermartingale_gaussNumeraire: the products ∏_{i=2}^t ℓ(Y_i) form a test supermartingale with respect to (𝒢_t);
• sec5_threshold_test_proof: the statement sec5_threshold_test.

theorem LogOptimal.isTestSupermartingale_gaussNumeraire {s : ℝ} (hs : 0 < s) : IsTestSupermartingale gaussNull helmertFiltration fun (t : ℕ) (x : ℕ → ℝ) => ∏ i ∈ Finset.Icc 2 t, lik s (helmertY i x)

The products ∏_{i=2}^t ℓ(Y_i) form a test supermartingale with respect to (𝒢_t), since they form a test martingale (Proposition 2).

theorem LogOptimal.sec5_threshold_test_proof (s : ℝ) : 0 < s → ∀ (α : ℝ), 0 < α → α ≤ 1 → ∀ P ∈ gaussNull, P {x : ℕ → ℝ | ∃ (t : ℕ), ENNReal.ofReal (1 / α) ≤ gaussNumeraire s t x} ≤ ENNReal.ofReal α