Documentation

LogOptimalEProcesses.Duality.Finite

Finite sample spaces and absolute continuity #

This file proves Proposition S1(i) of the paper (the converse in Remark 1) and the claims of Section S2.1 on finite sample spaces, following the proof of Proposition S1 in Section S2.1.

The proof of Proposition S1(i) is that of the paper, which adopted it after the formalization (its Section S5). For U = E/E*_t, the pointwise inequality u βˆ’ 1 βˆ’ log u β‰₯ (u^{1/2} βˆ’ 1)Β² gives E_Q[{U^{1/2} βˆ’ 1}Β²] ≀ E_Q(U) βˆ’ 1 βˆ’ E_Q(log U) ≀ R_t(E), and the e-processes are chosen with regrets at most 2^{βˆ’n}, so that the convergence is almost sure. For a finite 𝒳, the same argument is applied to the e-processes E^n set to zero at the nodes of Q-probability zero, which converge at every path to the versions of the numΓ©raires set to zero at these nodes.

Nodes of the tree of observations #

source
def LogOptimal.pathCylinder {𝒳 : Type u_1} (t : β„•) (x : β„• β†’ 𝒳) :
Set (β„• β†’ 𝒳)

The set of the paths whose first t observations are those of x, that is, the node x^t of the tree of depth t.

Equations
Instances For
    source
    theorem LogOptimal.mem_pathCylinder {𝒳 : Type u_1} {t : β„•} {x y : β„• β†’ 𝒳} :
    y ∈ pathCylinder t x ↔ βˆ€ i < t, y i = x i
    source
    theorem LogOptimal.mem_pathCylinder_self {𝒳 : Type u_1} (t : β„•) (x : β„• β†’ 𝒳) :
    x ∈ pathCylinder t x
    source
    theorem LogOptimal.pathCylinder_eq_of_mem {𝒳 : Type u_1} {t : β„•} {x y : β„• β†’ 𝒳} (h : y ∈ pathCylinder t x) :
    pathCylinder t y = pathCylinder t x
    source
    theorem LogOptimal.eq_of_mem_pathCylinder {𝒳 : Type u_1} [MeasurableSpace 𝒳] {Ξ² : Type u_2} [MeasurableSpace Ξ²] [MeasurableSingletonClass Ξ²] {t : β„•} {f : (β„• β†’ 𝒳) β†’ Ξ²} (hf : Measurable f) {x y : β„• β†’ 𝒳} (h : y ∈ pathCylinder t x) :
    f y = f x

    An β„±_t-measurable function takes the same value at two paths with the same first t observations.

    source
    theorem LogOptimal.measurableSet_pathCylinder {𝒳 : Type u_1} [MeasurableSpace 𝒳] [MeasurableSingletonClass 𝒳] (t : β„•) (x : β„• β†’ 𝒳) :
    MeasurableSet (pathCylinder t x)
    source
    theorem LogOptimal.measurable_dataFiltration_of_finite {𝒳 : Type u_1} [MeasurableSpace 𝒳] [Finite 𝒳] [MeasurableSingletonClass 𝒳] {Ξ² : Type u_2} [MeasurableSpace Ξ²] {t : β„•} {f : (β„• β†’ 𝒳) β†’ Ξ²} (hf : βˆ€ (x y : β„• β†’ 𝒳), y ∈ pathCylinder t x β†’ f y = f x) :
    Measurable f

    For a finite 𝒳, a function that is constant on the nodes of the tree of depth t is β„±_t-measurable.

    source
    theorem LogOptimal.measure_setOf_pathCylinder_eq_zero {𝒳 : Type u_1} [MeasurableSpace 𝒳] [Countable 𝒳] [MeasurableSingletonClass 𝒳] (Q : MeasureTheory.Measure (β„• β†’ 𝒳)) (t : β„•) :
    Q {x : β„• β†’ 𝒳 | Q (pathCylinder t x) = 0} = 0

    For a countable 𝒳, the paths at the nodes of Q-probability zero form a Q-null set.

    Null distributions that charge the sets of positive Q-probability #

    source
    theorem LogOptimal.FiniteOptimalEPower.exists_measure_ne_zero {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (β„• β†’ 𝒳))} {Q : MeasureTheory.Measure (β„• β†’ 𝒳)} (h𝔓 : βˆ€ P ∈ 𝔓, MeasureTheory.IsProbabilityMeasure P) (hfin : FiniteOptimalEPower 𝔓 Q) {t : β„•} {A : Set (β„• β†’ 𝒳)} (hA : MeasurableSet A) (hQA : Q A β‰  0) :
    βˆƒ P ∈ 𝔓, P A β‰  0

    Under the standing assumption, a set of β„±_t with positive Q-probability has positive probability under some null distribution (proof of Proposition S1(i)): otherwise 1 + ∞ 1(X^t ∈ B) would be an e-variable with infinite e-power. The paper takes 1 + m 1(X^t = x^t) and lets m β†’ ∞.

    Bounded e-processes stopped at T on a finite sample space #

    source
    theorem LogOptimal.measurableSet_pathCylinder_pos {𝒳 : Type u_1} [MeasurableSpace 𝒳] [Finite 𝒳] [MeasurableSingletonClass 𝒳] (Q : MeasureTheory.Measure (β„• β†’ 𝒳)) (t : β„•) :
    MeasurableSet {x : β„• β†’ 𝒳 | 0 < Q (pathCylinder t x)}

    For a finite 𝒳, the set of the paths at nodes of positive Q-probability is in β„±_t.

    source
    theorem LogOptimal.measurable_ite_pathCylinder_pos {𝒳 : Type u_1} [MeasurableSpace 𝒳] [Finite 𝒳] [MeasurableSingletonClass 𝒳] (Q : MeasureTheory.Measure (β„• β†’ 𝒳)) {t : β„•} {E : (β„• β†’ 𝒳) β†’ ENNReal} (hE : Measurable E) :
    Measurable fun (x : β„• β†’ 𝒳) => if 0 < Q (pathCylinder t x) then E x else 0

    A process set to zero at the nodes of Q-probability zero is still adapted.

    source
    theorem LogOptimal.ite_pathCylinder_pos_ae_eq {𝒳 : Type u_1} [MeasurableSpace 𝒳] [Finite 𝒳] [MeasurableSingletonClass 𝒳] (Q : MeasureTheory.Measure (β„• β†’ 𝒳)) (t : β„•) (E : (β„• β†’ 𝒳) β†’ ENNReal) :
    (fun (x : β„• β†’ 𝒳) => if 0 < Q (pathCylinder t x) then E x else 0) =ᡐ[Q] E

    A function set to zero at the nodes of Q-probability zero is Q-almost surely unchanged.

    source
    theorem LogOptimal.Setting.exists_bounded_stopped {𝒳 : Type u_1} [MeasurableSpace 𝒳] [Finite 𝒳] [MeasurableSingletonClass 𝒳] {𝔓 : Set (MeasureTheory.Measure (β„• β†’ 𝒳))} {Q : MeasureTheory.Measure (β„• β†’ 𝒳)} {Es : β„• β†’ (β„• β†’ 𝒳) β†’ ENNReal} (hS : Setting 𝔓 Q Es) {E : β„• β†’ (β„• β†’ 𝒳) β†’ ENNReal} (hE : IsEProcess 𝔓 E) (T : β„•) :
    βˆƒ (F : β„• β†’ (β„• β†’ 𝒳) β†’ ENNReal), (IsEProcess 𝔓 F ∧ (βˆ€ (t : β„•), F t = F (min t T)) ∧ βˆƒ (C : NNReal), βˆ€ (t : β„•) (x : β„• β†’ 𝒳), F t x ≀ ↑C) ∧ βˆ€ t ≀ T, regret Q (Es t) (F t) = regret Q (Es t) (E t)

    For a finite 𝒳, every e-process (E_t) has a bounded version (F_t) stopped at T with the same regrets at t ≀ T (proof of Proposition S1(i)): (E_{t∧T}) set to zero at the nodes of Q-probability zero. At a node x^t of positive Q-probability, some null distribution P has P(X^t = x^t) > 0, and E_t(x^t) ≀ 1/P(X^t = x^t).

    Almost sure convergence from summable regrets #

    source
    theorem LogOptimal.ofReal_sqrt_sub_one_sq_add_le (y : ENNReal) :
    ENNReal.ofReal ((√y.toReal - 1) ^ 2) + 1 + y.log.toENNReal ≀ y + (-y.log).toENNReal

    The pointwise inequality (u^{1/2} βˆ’ 1)Β² + 1 + log⁺ u ≀ u + log⁻ u in [0, ∞], that is, (u^{1/2} βˆ’ 1)Β² ≀ u βˆ’ 1 βˆ’ log u, which follows from log u^{1/2} ≀ u^{1/2} βˆ’ 1.

    source
    theorem LogOptimal.tendsto_one_of_tsum_sqrt_sub_one_sq_ne_top {u : β„• β†’ ENNReal} (h : βˆ‘' (n : β„•), ENNReal.ofReal ((√(u n).toReal - 1) ^ 2) β‰  ⊀) :
    Filter.Tendsto u Filter.atTop (nhds 1)

    If βˆ‘_n (u_n^{1/2} βˆ’ 1)Β² < ∞, then u_n β†’ 1.

    source
    theorem LogOptimal.Setting.lintegral_sqrt_sub_one_sq_le {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (β„• β†’ 𝒳))} {Q : MeasureTheory.Measure (β„• β†’ 𝒳)} {Es : β„• β†’ (β„• β†’ 𝒳) β†’ ENNReal} (hS : Setting 𝔓 Q Es) {t : β„•} {E : (β„• β†’ 𝒳) β†’ ENNReal} (hE : IsEVariable 𝔓 t E) {Ξ΅ : ℝ} (hΞ΅ : 0 ≀ Ξ΅) (hR : regret Q (Es t) E ≀ ↑Ρ) :
    ∫⁻ (x : β„• β†’ 𝒳), ENNReal.ofReal ((√(E x / Es t x).toReal - 1) ^ 2) βˆ‚Q ≀ ENNReal.ofReal Ξ΅

    For E ∈ β„°_t and U = E/E*_t, E_Q[{U^{1/2} βˆ’ 1}Β²] ≀ E_Q(U) βˆ’ 1 βˆ’ E_Q(log U) ≀ R_t(E) (proof of Proposition S1(i)).

    source
    theorem LogOptimal.Setting.exists_measurableSet_tendsto {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (β„• β†’ 𝒳))} {Q : MeasureTheory.Measure (β„• β†’ 𝒳)} {Es : β„• β†’ (β„• β†’ 𝒳) β†’ ENNReal} (hS : Setting 𝔓 Q Es) {t : β„•} {F : β„• β†’ (β„• β†’ 𝒳) β†’ ENNReal} (hF : βˆ€ (n : β„•), IsEVariable 𝔓 t (F n)) (hR : βˆ€ (n : β„•), regret Q (Es t) (F n) ≀ ↑(2⁻¹ ^ n)) :
    βˆƒ (G : Set (β„• β†’ 𝒳)), MeasurableSet G ∧ Q Gᢜ = 0 ∧ βˆ€ x ∈ G, 0 < Es t x ∧ Filter.Tendsto (fun (n : β„•) => F n x) Filter.atTop (nhds (Es t x))

    Almost sure convergence from summable regrets (proof of Proposition S1(i)): if E^n ∈ β„°_t and R_t(E^n) ≀ 2^{βˆ’n}, then E^n β†’ E*_t on a set of β„±_t of full Q-probability, on which E*_t > 0.

    Proposition S1(i) #

    source
    theorem LogOptimal.measure_eq_zero_of_marginal_ac {𝒳 : Type u_1} [MeasurableSpace 𝒳] {Q P : MeasureTheory.Measure (β„• β†’ 𝒳)} {T : β„•} (hPQ : (marginal P T).AbsolutelyContinuous (marginal Q T)) {A : Set (β„• β†’ 𝒳)} (hA : MeasurableSet A) (hQA : Q A = 0) :
    P A = 0

    If P_T β‰ͺ Q_T, a Q-null set of β„±_T is P-null.

    source
    theorem LogOptimal.Setting.exists_isEProcess_versions {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (β„• β†’ 𝒳))} {Q : MeasureTheory.Measure (β„• β†’ 𝒳)} {Es : β„• β†’ (β„• β†’ 𝒳) β†’ ENNReal} (hS : Setting 𝔓 Q Es) {T : β„•} (hΞ“ : minimaxRegret 𝔓 Q Es T = 0) (h𝒳 : Finite 𝒳 ∧ MeasurableSingletonClass 𝒳 ∨ βˆ€ P ∈ 𝔓, (marginal P T).AbsolutelyContinuous (marginal Q T)) :
    βˆƒ (Es' : β„• β†’ (β„• β†’ 𝒳) β†’ ENNReal), (βˆ€ t ≀ T, Measurable (Es' t) ∧ Es' t =ᡐ[Q] Es t) ∧ IsEProcess 𝔓 fun (t : β„•) => Es' (min t T)

    Proposition S1(i): if Ξ“_T = 0, and 𝒳 is finite or every P_T is absolutely continuous with respect to Q_T, then E*_0, …, E*_T have versions such that (E*_{t∧T})_{tβ‰₯0} is an e-process. In the second case, the versions are any versions; in the first case, the numΓ©raires are set to zero at the nodes of Q-probability zero.

    The claims of Section S2.1 on finite sample spaces #

    source
    theorem LogOptimal.sec_finite_bounded_proof (𝒳 : Type u) [MeasurableSpace 𝒳] [Finite 𝒳] [MeasurableSingletonClass 𝒳] (𝔓 : Set (MeasureTheory.Measure (β„• β†’ 𝒳))) (Q : MeasureTheory.Measure (β„• β†’ 𝒳)) (Es : β„• β†’ (β„• β†’ 𝒳) β†’ ENNReal) :
    Setting 𝔓 Q Es β†’ βˆ€ (T : β„•), minimaxRegret 𝔓 Q Es T = β¨… (E : β„• β†’ (β„• β†’ 𝒳) β†’ ENNReal), β¨… (_ : IsEProcess 𝔓 E ∧ (βˆ€ (t : β„•), E t = E (min t T)) ∧ βˆƒ (C : NNReal), βˆ€ (t : β„•) (x : β„• β†’ 𝒳), E t x ≀ ↑C), ⨆ (t : β„•), ⨆ (_ : t ≀ T), regret Q (Es t) (E t)
    source
    theorem LogOptimal.sec_finite_disjoint_proof (𝒳 : Type u) [MeasurableSpace 𝒳] (Q : MeasureTheory.Measure (β„• β†’ 𝒳)) (T : β„•) (t t' : Fin (T + 1)) :
    t β‰  t' β†’ (stoppedAlternative Q T (Pi.single t 1)).MutuallySingular (stoppedAlternative Q T (Pi.single t' 1))