OAI/Analysis/Conductivity/Sources/IteratedAverages.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.sourceAveragePullIter_mean_bound line 13
2. lemma OAI.ScalarConductivity.sourceAveragePullIter_mean_eq line 31
3. lemma OAI.ScalarConductivity.sourceAverageDifference_mean_bound line 41
4. lemma OAI.ScalarConductivity.BoundedRootSources.finiteSource_weighted_bound line 57
5. lemma OAI.ScalarConductivity.BoundedRootSources.form_weighted_test line 80
6. theorem OAI.ScalarConductivity.BoundedRootSources.nested_source_weighted line 91
7. lemma OAI.ScalarConductivity.sourceRootBoundary_mem_closure line 126
8. lemma OAI.ScalarConductivity.sourceWordBoundary_mem_cell line 132
9. lemma OAI.ScalarConductivity.sourceWordMean_smooth_constant line 136
10. lemma OAI.ScalarConductivity.source_first_children_separator line 145
11. lemma OAI.ScalarConductivity.BoundedRootSources.finiteSource_separator line 165
12. lemma OAI.ScalarConductivity.BoundedRootSources.nested_source_nonzero line 181