OAI/Combinatorics/Progressions/Geometry/SupportedFiberApproximation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_integrable_of_support line 15
2. theorem OAI.Erdos3.FiniteProbabilityWeights.integral_complexMean_of_support line 25
3. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_supported_fiber_l1_error line 51
4. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_supported_fiber_l1_error_uniform line 110
5. theorem OAI.Erdos3.FiniteProbabilityWeights.exists_mem_positive_fiber line 134
6. theorem OAI.Erdos3.FiniteProbabilityWeights.exists_supported_fiber_l1_approximation line 139