OAI/Analysis/IntegralMeans/PositiveArea.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Brennan.schlicht_bracketSq_growthline 10 - lemma
OAI.Brennan.continuousOn_smoothPower_compline 26 - lemma
OAI.Brennan.schlicht_function_arealine 30 - lemma
OAI.Brennan.bracketSq_negative_integrableline 92 - lemma
OAI.Brennan.schlicht_weighted_derivative_integrableline 102 - lemma
OAI.Brennan.schlicht_positive_arealine 119