BKDyadic.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.GammaFPP.BK.survival_le_one line 9
def OAI.GammaFPP.BK.BitGood line 15
Source documentation
The guard implements infinity at zero; D's totalized value at zero is unused.
```
def BitGood (D : ℝ → ℝ) (t : ℕ) (x : Finset (Edge × Fin t))
    (p : StrictPathWitness) : Prop :=
…
```
Mentions: OAI.GammaFPP.BK.StrictPathWitness
lemma OAI.GammaFPP.BK.bitGood_mono line 20
lemma OAI.GammaFPP.BK.bitGood_of_agree line 32
def OAI.GammaFPP.BK.bitFamily line 50
lemma OAI.GammaFPP.BK.mem_bitFamily line 56
lemma OAI.GammaFPP.BK.upward_bitFamily line 63
lemma OAI.GammaFPP.BK.bit_path_forces line 73
def OAI.GammaFPP.BK.bitDisjointFamily line 80

theorem OAI.GammaFPP.BK.decoder_finite_path_BK line 89

Source documentation

Repeated labelled families are allowed: independence of events is not assumed.

theorem decoder_finite_path_BK {D : ℝ → ℝ} (hD : AntitoneOn D (Ioc 0 1))
    (S : Finset Edge) (t : ℕ) (Fs : List (Set StrictPathWitness)) :
    fairFamilyMass (S.product (Finset.univ : Finset (Fin t))) (bitDisjointFamily D S t Fs) ≤
      (Fs.map (fun F => fairFamilyMass (S.product (Finset.univ : Finset (Fin t))) (bitFamily D S t F))).prod := by
…

Mentions: OAI.GammaFPP.BK.StrictPathWitness, OAI.GammaFPP.BK.bitDisjointFamily, OAI.GammaFPP.BK.bitFamily

theorem OAI.GammaFPP.BK.gamma_decoder_finite_path_BK line 112

Source documentation

Actual Gamma decoder, for every positive shape and rate.

theorem gamma_decoder_finite_path_BK {shape rate : ℝ} (hs : 0 < shape) (hr : 0 < rate)
    (S : Finset Edge) (t : ℕ) (Fs : List (Set StrictPathWitness)) :
    fairFamilyMass (S.product (Finset.univ : Finset (Fin t))) (bitDisjointFamily (gammaSurvivalQuantile hs hr) S t Fs) ≤
      (Fs.map (fun F => fairFamilyMass (S.product (Finset.univ : Finset (Fin t)))
        (bitFamily (gammaSurvivalQuantile hs hr) S t F))).prod :=
…

Mentions: OAI.GammaFPP.BK.StrictPathWitness, OAI.GammaFPP.BK.bitDisjointFamily, OAI.GammaFPP.gammaSurvivalQuantile, OAI.GammaFPP.BK.bitFamily