OAI/MeasureTheory/DyadicAvoidance/SelectorMoment.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem310.SelectorMoment.product_eq_pow_active line 14
2. theorem OAI.Problem310.SelectorMoment.independent_boolean_moment line 20

   Source documentation

   Exponential moment of the number of active independent Boolean trials.

   theorem independent_boolean_moment
       {Ω : Type u_Ω} {I : Type u_I} [MeasurableSpace Ω] [Fintype I] [DecidableEq I]
       [MeasurableSpace Bool] [MeasurableSingletonClass Bool]
       (μ : Measure Ω) [IsProbabilityMeasure μ] (ν : Measure Bool)
       (X : I → Ω → Bool) (hX : iIndepFun X μ)
       (hXm : ∀ i, Measurable (X i)) (hmap : ∀ i, μ.map (X i) = ν)
       (q : ℝ≥0∞) :
       (∫⁻ ω, q ^ Fintype.card {i // X i ω = true} ∂μ) =
         (ν {false} + q * ν {true}) ^ Fintype.card I := by
   …

3. theorem OAI.Problem310.SelectorMoment.lookup_boolean_moment line 48

   Source documentation

   The same moment for injective coordinate lookups in a larger product table.

   theorem lookup_boolean_moment
       {I : Type u_I} {K : Type u_K} [Fintype I] [DecidableEq I] [Fintype K]
       [MeasurableSpace Bool] [MeasurableSingletonClass Bool]
       (ν : Measure Bool) [IsProbabilityMeasure ν]
       (addr : I → K) (hinj : Function.Injective addr) (q : ℝ≥0∞) :
       (∫⁻ ω : K → Bool, q ^ Fintype.card {i // ω (addr i) = true}
         ∂(Measure.pi (fun _ : K => ν))) =
         (ν {false} + q * ν {true}) ^ Fintype.card I := by
   …

4. theorem OAI.Problem310.SelectorMoment.lookup_fair_moment line 65

   Source documentation

   Fair fresh selector entries, with an arbitrary nonnegative failure factor.

   theorem lookup_fair_moment
       {I : Type u_I} {K : Type u_K} [Fintype I] [DecidableEq I] [Fintype K]
       [MeasurableSpace Bool] [MeasurableSingletonClass Bool]
       (ν : Measure Bool) [IsProbabilityMeasure ν]
       (hfalse : ν {false} = 1 / 2) (htrue : ν {true} = 1 / 2)
       (addr : I → K) (hinj : Function.Injective addr) (q : ℝ≥0∞) :
       (∫⁻ ω : K → Bool, q ^ Fintype.card {i // ω (addr i) = true}
         ∂(Measure.pi (fun _ : K => ν))) =
         (1 / 2 + q / 2) ^ Fintype.card I := by
   …

5. theorem OAI.Problem310.SelectorMoment.lookup_fair_failure_moment line 78

   Source documentation

   The exact fixed-scale base, with real parameter p.

   theorem lookup_fair_failure_moment
       {I : Type u_I} {K : Type u_K} [Fintype I] [DecidableEq I] [Fintype K]
       [MeasurableSpace Bool] [MeasurableSingletonClass Bool]
       (ν : Measure Bool) [IsProbabilityMeasure ν]
       (hfalse : ν {false} = 1 / 2) (htrue : ν {true} = 1 / 2)
       (addr : I → K) (hinj : Function.Injective addr)
       (p : ℝ) (hp : p ≤ 1) :
       (∫⁻ ω : K → Bool, (ENNReal.ofReal (1 - p)) ^ Fintype.card {i // ω (addr i) = true}
         ∂(Measure.pi (fun _ : K => ν))) =
         (ENNReal.ofReal (1 - p / 2)) ^ Fintype.card I := by
   …