OAI/Analysis/Conductivity/Fourier/FourierMatchingElliptic.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.matrix_quadratic_elementwise_bound line 13
2. lemma OAI.ScalarConductivity.flatBackgroundTensor_lower line 38
3. lemma OAI.ScalarConductivity.flatBackgroundTensor_small_perturbation line 45
4. theorem OAI.ScalarConductivity.elliptic_fourier_matching line 61
5. theorem OAI.ScalarConductivity.smooth_fourier_matching_with_origin line 125