OAI/Analysis/ProductSpaces/ConditionalBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentProducts.firstExitSum line 19

   Source documentation

   A finite first-exit polynomial on conditionally independent coefficient blocks.

   def firstExitSum (B : ι → Ω → ℝ) (z : (ι → Ω) × (ι → ℝ)) : ℝ :=
   …

2. lemma OAI.IndependentProducts.measurable_firstExitSum line 22
3. lemma OAI.IndependentProducts.integrable_firstExitSum line 29
4. lemma OAI.IndependentProducts.first_exit_scalar_bound line 41
5. lemma OAI.IndependentProducts.real_midpoint_excess line 73
6. lemma OAI.IndependentProducts.midpointGain_eq_integral_excess line 78
7. lemma OAI.IndependentProducts.integrated_first_exit_affine line 124