OAI/Probability/Ballisticity/Stationary/ArrayMassSurvival.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.arrayProfileMass_total_le_one line 14
2. lemma OAI.DirectionalTransience.upperHorizontalKernel_mass_sum line 23
3. lemma OAI.DirectionalTransience.arrayKernelImage_total_le_discount line 29
4. lemma OAI.DirectionalTransience.arraySelfMass_mul_q_le_discount line 49
5. def OAI.DirectionalTransience.arrayCurrentData line 68
6. lemma OAI.DirectionalTransience.arrayCurrentData_measurable line 70
7. lemma OAI.DirectionalTransience.typedCurrentArrayWindow_data line 72
8. lemma OAI.DirectionalTransience.ennreal_negative_power_exp_lower line 75
9. lemma OAI.DirectionalTransience.selfmass_nodrop_bound line 83
10. lemma OAI.DirectionalTransience.array_selectedProduct_lower line 101