Cond bind le of forall le
Prob.cond_bind_le_of_forall_le
Plain-language statement
We can bound a cond bind uniformly in the first argument
Exact Lean statement
lemma cond_bind_le_of_forall_le {f : Prob α} {g : α → Prob β} {p q : β → Prop} {b : ℝ}
(b0 : 0 ≤ b) (le : ∀ x, f.prob x ≠ 0 → (g x).cond p q ≤ b) : (f >>= g).cond p q ≤ bFormal artifact
Lean source
lemma cond_bind_le_of_forall_le {f : Prob α} {g : α → Prob β} {p q : β → Prop} {b : ℝ} (b0 : 0 ≤ b) (le : ∀ x, f.prob x ≠ 0 → (g x).cond p q ≤ b) : (f >>= g).cond p q ≤ b := by simp only [cond] by_cases fg0 : 0 < (f >>= g).pr q · simp only [div_le_iff fg0]; simp only [pr, ←exp_const_mul, exp_bind] apply exp_mono; intro x px; specialize le x px; simp only [exp_const_mul] by_cases g0 : 0 < (g x).pr q · simp only [cond, div_le_iff g0] at le; exact le · replace g0 := le_antisymm (not_lt.mp g0) pr_nonneg; simp only [pr] at g0 simp only [g0, mul_zero]; nth_rewrite 2 [←g0] apply exp_mono; intro y _; simp only [ite_le_ite_iff]; exact And.right · replace fg0 := le_antisymm (not_lt.mp fg0) pr_nonneg simp only [fg0, div_zero, b0]- Project
- debate
- License
- Apache-2.0
- Commit
- de3a6e500ae1
- Source
- Prob/Cond.lean:85-97
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Alice pr le
alice_pr_le
Plain-language statement
Honest Alice has error ≥ e with probability ≤ q
Source project: debate
Person-level attribution pending.
Alice steps cost
alice_steps_cost
Plain-language statement
Alice makes few queries, regardless of Bob and Vera
Source project: debate
Person-level attribution pending.
Alices close
alices_close
Plain-language statement
Alice produces (p,y) with p close to o.probs y with good probability
Source project: debate
Person-level attribution pending.