OAI/Analysis/Conductivity/Fourier/CompactifiedFourierTail.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.linear_comp_iterated_point_bound line 12
2. lemma OAI.ScalarConductivity.glue_derivative_compact_bound line 23
3. lemma OAI.ScalarConductivity.glue_scaled_iterated_bound line 32
4. lemma OAI.ScalarConductivity.flatPhaseMode_shift_snd_bound line 58
5. def OAI.ScalarConductivity.compactifiedFourierTerm line 79
6. def OAI.ScalarConductivity.compactifiedFourierTail line 84
7. lemma OAI.ScalarConductivity.compactifiedFourierTerm_smooth line 88
8. lemma OAI.ScalarConductivity.compactifiedFourierTerm_iterated_bound line 95
9. theorem OAI.ScalarConductivity.compactifiedFourierTail_smooth line 135
10. lemma OAI.ScalarConductivity.compactifiedFourierTail_of_pos line 158
11. lemma OAI.ScalarConductivity.compactifiedFourierTail_of_nonpos line 185