Experimentation.Sequential

theorem supermartingale_maximal_ineq [IsFiniteMeasure μ] {M : ℕ → Ω → ℝ} (hM : Supermartingale M ℱ μ) (hnonneg : ∀ n, 0 ≤ M n) {lam : ℝ} (hlam : 0 < lam) (n : ℕ) : μ {ω | lam ≤ (range (n + 1)).sup' nonempty_range_add_one (fun k => M k ω)} ≤ ofReal (μ[M 0] / lam) := by classical let τ : Ω → ℕ∞ := fun ω => (hittingBtwn M {y : ℝ | lam ≤ y} (0 : ℕ) n ω : ℕ) let A : Set Ω := {ω | lam ≤ (range (n + 1)).sup' nonempty_range_add_one (fun k => M k ω)} have hAmeas : MeasurableSet A := by exact measurableSet_le measurable_const (Finset.measurable_range_sup'' fun k _ => (hM.1.stronglyMeasurable (i := k)).measurable) have hτstop : IsStoppingTime ℱ τ := by exact hM.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici have hτbdd : ∀ ω, τ ω ≤ n := by intro ω simpa [τ] using (show (((hittingBtwn M {y : ℝ | lam ≤ y} (0 : ℕ) n ω : ℕ) : ℕ∞) ≤ (n : ℕ∞)) from by exact WithTop.coe_le_coe.2 (hittingBtwn_le (u := M) (s := {y : ℝ | lam ≤ y}) (n := (0 : ℕ)) (m := n) (ω := ω))) have hτint : Integrable (stoppedValue M τ) μ := integrable_stoppedValue ℕ hτstop hM.2.2 hτbdd have hhit : ∀ ω ∈ A, lam ≤ stoppedValue M τ ω := by intro ω hω simp_rw [A, Set.mem_setOf_eq, Finset.le_sup'_iff, Finset.mem_range, Nat.lt_succ_iff] at hω refine stoppedValue_hittingBtwn_mem ?_ simpa only [Set.mem_setOf_eq, Set.mem_Icc, zero_le, true_and] using hω have hsetLower : lam * (μ A).toReal ≤ ∫ ω in A, stoppedValue M τ ω ∂μ := setIntegral_ge_of_const_le_real hAmeas (measure_ne_top _ _) hhit hτint.integrableOn have hstopped_nonneg : 0 ≤ stoppedValue M τ := by intro ω exact hnonneg _ ω have hset_le_total : ∫ ω in A, stoppedValue M τ ω ∂μ ≤ μ[stoppedValue M τ] := by have hcompl_nonneg : 0 ≤ ∫ ω in Aᶜ, stoppedValue M τ ω ∂μ := setIntegral_nonneg hAmeas.compl fun ω _ => hstopped_nonneg ω have hadd := integral_add_compl hAmeas hτint linarith have hτ_le_M0 : μ[stoppedValue M τ] ≤ μ[M 0] := by have hneg : Submartingale (fun k ω => -M k ω) ℱ μ := hM.neg have hopt : μ[stoppedValue (fun k ω => -M k ω) (fun _ : Ω => ((0 : ℕ) : ℕ∞))] ≤ μ[stoppedValue (fun k ω => -M k ω) τ] := by refine hneg.expected_stoppedValue_mono (isStoppingTime_const ℱ 0) hτstop ?_ hτbdd intro ω simp [τ] have hleft : μ[stoppedValue (fun k ω => -M k ω) (fun _ : Ω => ((0 : ℕ) : ℕ∞))] = - μ[M 0] := by rw [show stoppedValue (fun k ω => -M k ω) (fun _ : Ω => ((0 : ℕ) : ℕ∞)) = fun ω => -M 0 ω by funext ω simp only [stoppedValue] rfl] exact integral_neg (M 0) have hright : μ[stoppedValue (fun k ω => -M k ω) τ] = - μ[stoppedValue M τ] := by rw [show stoppedValue (fun k ω => -M k ω) τ = fun ω => - stoppedValue M τ ω by funext ω simp [stoppedValue]] exact integral_neg (stoppedValue M τ) rw [hleft, hright] at hopt linarith have hmul : lam * (μ A).toReal ≤ μ[M 0] := hsetLower.trans (hset_le_total.trans hτ_le_M0) have hM0_nonneg : 0 ≤ μ[M 0] := integral_nonneg (hnonneg 0) have hdiv_nonneg : 0 ≤ μ[M 0] / lam := div_nonneg hM0_nonneg hlam.le change μ A ≤ ofReal (μ[M 0] / lam) rw [ENNReal.le_ofReal_iff_toReal_le (measure_ne_top _ _) hdiv_nonneg] exact (le_div_iff₀ hlam).2 (by simpa [mul_comm] using hmul)

theorem ville_test [IsFiniteMeasure μ] {M : ℕ → Ω → ℝ} (hM : IsTestSupermartingale M ℱ μ) {α : ℝ} (hα : 0 < α) : μ {ω | ∃ n, 1 / α ≤ M n ω} ≤ ofReal α := by obtain ⟨hsuper, hnn, hM0⟩ := hM have hlam : (0 : ℝ) < 1 / α := by positivity refine le_trans (ville_inequality hsuper hnn hlam) ?_ apply ENNReal.ofReal_le_ofReal rw [div_div_eq_mul_div, div_one] calc μ[M 0] * α ≤ 1 * α := mul_le_mul_of_nonneg_right hM0 hα.le _ = α := one_mul α