OAI/Analysis/Conductivity/Fourier/FourierMatchingLocalData.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.flatTensorLaplacian_congr_nhds line 12
2. lemma OAI.ScalarConductivity.fourier_left_coeff_bound line 16
3. lemma OAI.ScalarConductivity.fourierMatchingPair_left_fourier line 21
4. lemma OAI.ScalarConductivity.fourierMatchingPair_right_fourier line 44
5. lemma OAI.ScalarConductivity.periodicSourceMoment_neg line 66
6. theorem OAI.ScalarConductivity.fourier_matching_three_moments line 80
7. lemma OAI.ScalarConductivity.fourierMatchingResidual_exact line 126
8. lemma OAI.ScalarConductivity.fourier_single_plus_rate line 164
9. lemma OAI.ScalarConductivity.fourierMatchingResidual_moments line 174