OAI/Analysis/ProductSpaces/MidpointModulus.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentProducts.midpointGain line 16
2. lemma OAI.IndependentProducts.midpointGain_nonneg line 18
3. lemma OAI.IndependentProducts.midpointGain_le line 26
4. lemma OAI.IndependentProducts.midpointGain_center_bound line 33
5. lemma OAI.IndependentProducts.continuous_midpointGain line 46
6. lemma OAI.IndependentProducts.affine_on_closed_tail line 50
7. lemma OAI.IndependentProducts.exists_unit_of_not_finiteDimensional line 57
8. lemma OAI.IndependentProducts.cofinite_exists_unit line 66
9. lemma OAI.IndependentProducts.averagedModulus_lower_of_approx line 77
10. lemma OAI.IndependentProducts.averagedModulus_of_dense_affine line 129