OAI/Analysis/Conductivity/Scalarization/WeakCellFast.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.integral_norm_le_L2_const line 13
2. lemma OAI.ScalarConductivity.compact_inner_right line 34
3. lemma OAI.ScalarConductivity.vector_pairing_bound_of_zero_mean line 42
4. lemma OAI.ScalarConductivity.norm_finite_disjoint_sum line 70
5. lemma OAI.ScalarConductivity.finite_cell_pairing_bound line 89
6. lemma OAI.ScalarConductivity.fine_cell_pairing_bound line 122
7. lemma OAI.ScalarConductivity.inner_tendsto_zero_of_dense_tests line 158
8. lemma OAI.ScalarConductivity.fine_cells_continuous_pairing_tendsto_zero line 190