Documentation

LogOptimalEProcesses.Examples.Models

Two models that satisfy the hypotheses of the general results #

The general results of Sections 1 to 3 of the paper and of Section S2.1 assume the standing assumption of Section 2 (Setting), and the results on finite sample spaces assume, moreover, that 𝒳 is finite. Two models satisfy these hypotheses.

The Gaussian location model #

source
theorem LogOptimal.Examples.gauss_minimaxRegret_le_log_succ {s ρ : ℝ} (hs : 0 < s) (hρ : 1 - s ^ 2 ≀ ρ ^ 2) (T : β„•) :
minimaxRegret gaussNull (mixAlt s ρ) (gaussNumeraire s) T ≀ ↑(Real.log (↑T + 1))

A model of coin tosses #

source
noncomputable def LogOptimal.Examples.coinHalf :
↑unitInterval

The probability 1/2 of true of a fair coin.

Equations
Instances For
    source
    noncomputable def LogOptimal.Examples.coinQuarter :
    ↑unitInterval

    The probability 1/4 of true of the coins of the alternative.

    Equations
    Instances For
      source
      noncomputable def LogOptimal.Examples.coinNull :
      MeasureTheory.Measure (β„• β†’ Bool)

      The distribution of independent fair coins, the simple null of the coin model.

      Equations
      Instances For
        source
        noncomputable def LogOptimal.Examples.coinAlt :
        MeasureTheory.Measure (β„• β†’ Bool)

        The distribution of independent coins with probability 1/4 of true, the alternative of the coin model.

        Equations
        Instances For
          source
          noncomputable def LogOptimal.Examples.coinNumeraire (t : β„•) (x : β„• β†’ Bool) :
          ENNReal

          The numΓ©raires of the coin model: the likelihood ratios dQ_t/dP_t at X^t.

          Equations
          Instances For
            source
            instance LogOptimal.Examples.instIsProbabilityMeasureForallNatBoolCoinNull :
            MeasureTheory.IsProbabilityMeasure coinNull

            The null of the coin model is a probability measure.

            source
            instance LogOptimal.Examples.instIsProbabilityMeasureForallNatBoolCoinAlt :
            MeasureTheory.IsProbabilityMeasure coinAlt

            The alternative of the coin model is a probability measure.

            source
            theorem LogOptimal.Examples.bernoulliMeasure_coinHalf_singleton (b : Bool) :
            (ProbabilityTheory.bernoulliMeasure true false coinHalf) {b} = 2⁻¹
            source
            theorem LogOptimal.Examples.coinNull_pathCylinder (t : β„•) (x : β„• β†’ Bool) :
            coinNull (pathCylinder t x) = 2⁻¹ ^ t
            source
            theorem LogOptimal.Examples.le_two_pow_of_isEVariable_coin {t : β„•} {E : (β„• β†’ Bool) β†’ ENNReal} (hE : IsEVariable {coinNull} t E) (x : β„• β†’ Bool) :
            E x ≀ 2 ^ t
            source
            theorem LogOptimal.Examples.finiteOptimalEPower_coin :
            FiniteOptimalEPower {coinNull} coinAlt
            source
            theorem LogOptimal.Examples.setting_coin :
            Setting {coinNull} coinAlt coinNumeraire
            source
            theorem LogOptimal.Examples.coin_minimaxRegret_eq_zero (T : β„•) :
            minimaxRegret {coinNull} coinAlt coinNumeraire T = 0
            source
            theorem LogOptimal.Examples.coin_exists_isEProcess_versions (T : β„•) :
            βˆƒ (Es' : β„• β†’ (β„• β†’ Bool) β†’ ENNReal), (βˆ€ t ≀ T, Measurable (Es' t) ∧ Es' t =ᡐ[coinAlt] coinNumeraire t) ∧ IsEProcess {coinNull} fun (t : β„•) => Es' (min t T)
            source
            theorem LogOptimal.Examples.coin_exists_maximin (T : β„•) :
            βˆƒ ΞΎ ∈ probVectors T, minimaxRegret {coinNull} coinAlt coinNumeraire T = β¨… (E : β„• β†’ (β„• β†’ Bool) β†’ ENNReal), β¨… (_ : IsEProcess {coinNull} E), βˆ‘ t : Fin (T + 1), ↑(ΞΎ t) * regret coinAlt (coinNumeraire ↑t) (E ↑t)
            source
            theorem LogOptimal.Examples.coin_minimaxRegret_eq_iInf_bounded (T : β„•) :
            minimaxRegret {coinNull} coinAlt coinNumeraire T = β¨… (E : β„• β†’ (β„• β†’ Bool) β†’ ENNReal), β¨… (_ : IsEProcess {coinNull} E ∧ (βˆ€ (t : β„•), E t = E (min t T)) ∧ βˆƒ (C : NNReal), βˆ€ (t : β„•) (x : β„• β†’ Bool), E t x ≀ ↑C), ⨆ (t : β„•), ⨆ (_ : t ≀ T), regret coinAlt (coinNumeraire t) (E t)