OAI/Analysis/Conductivity/Flux/TorusBoxFlux.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ScalarConductivity.torusCellIntegral line 12
2. lemma OAI.ScalarConductivity.integral_coord2_Icc line 15
3. lemma OAI.ScalarConductivity.integral_coord3_Icc line 46
4. lemma OAI.ScalarConductivity.coordinateDivergence_eq_trace line 84
5. theorem OAI.ScalarConductivity.torus_band_divergence line 91
6. lemma OAI.ScalarConductivity.smooth_smul_of_support_in_open line 147
7. lemma OAI.ScalarConductivity.axial_band_smooth_extension line 161
8. lemma OAI.ScalarConductivity.coordinateDivergence_congr_nhds line 190
9. theorem OAI.ScalarConductivity.torus_band_divergence_halfspace line 198
10. lemma OAI.ScalarConductivity.torus_flux_constant line 227
11. lemma OAI.ScalarConductivity.torus_flux_zero_of_tendsto line 242