OAI/Analysis/FourierLLogL/Thermal/Reference.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FourierLLogL.Dyadic.Thermal.clones_eq line 12
2. lemma OAI.FourierLLogL.Dyadic.Thermal.clones_pos line 14
3. def OAI.FourierLLogL.Dyadic.Thermal.observationBudget line 16
4. lemma OAI.FourierLLogL.Dyadic.Thermal.obs_scale line 18
5. lemma OAI.FourierLLogL.Dyadic.Thermal.alarm_scale line 37
6. theorem OAI.FourierLLogL.Dyadic.Thermal.conditional_bound line 92

   Source documentation

   Probability form: unnormalized comparison weights are tune × 1_p

   theorem conditional_bound (C : ℝ) (hC : 1 ≤ C) :
       ∀ᶠ j : ℕ in atTop, ∀ M : ℕ, ∀ p : Node,
       ∀ A : Form M, Press C j p A → 1000*p.invlen ≤ 2^M →
       ∀ P : Law (Grid M), ∀ u : Update j M p, u.Good C A P →
         u.regular → ∀ s : Profile M,
         (∀ i∈s, 0 ≤ i.1 ∧ i.1 ≤ A) → s.length ≤ observationBudget C j →
         admissible s p (cushion j) → ∀ z : Grid M,
         expU (fun x => prefixE s p x * u.alarmQ A z x) ≤
           exp (-(u.credit/8)) * expU (prefixE s p) := by
   …

   Mentions: OAI.FourierLLogL.Dyadic.Node, OAI.FourierLLogL.Dyadic.Thermal.Form, OAI.FourierLLogL.Dyadic.Thermal.Press, OAI.FourierLLogL.Law, OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.Thermal.Update, OAI.FourierLLogL.Dyadic.Thermal.Profile, OAI.FourierLLogL.Dyadic.Thermal.observationBudget, OAI.FourierLLogL.Dyadic.Thermal.admissible, OAI.FourierLLogL.Dyadic.Thermal.cushion, OAI.FourierLLogL.Dyadic.expU, OAI.FourierLLogL.Dyadic.Thermal.prefixE