OAI/Analysis/Conductivity/Geometry/BoxMomentRightInverse.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.exists_unit_global_interval_bump line 13
2. lemma OAI.ScalarConductivity.exists_unit_box_bump line 25
3. lemma OAI.ScalarConductivity.cubePartial_integral_zero line 54
4. theorem OAI.ScalarConductivity.box_moment_right_inverse line 60
5. theorem OAI.ScalarConductivity.box_moment_bounded_right_inverse line 120