OAI/Probability/FreeIsing/Trees/IndexedPathVariance.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.sum_indexed_translate_le_tsum line 12
2. theorem OAI.Problem367.norm_sum_sq_le_geometric_bound_of_injective_index line 26
3. theorem OAI.Problem367.integral_sum_sq_le_geometric_bound_of_injective_index line 42
4. theorem OAI.Problem367.norm_sum_fin_sq_le_geometric_inner_bound line 60
5. theorem OAI.Problem367.integral_sum_fin_sq_le_geometric_pair_bound line 74
6. theorem OAI.Problem367.norm_sum_fin_sq_le_ordered_geometric_inner_bound line 90
7. theorem OAI.Problem367.integral_sum_fin_sq_le_ordered_geometric_pair_bound line 107