OAI/Analysis/Conductivity/Fourier/PeriodicFamilyCorrection.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.correctionBox_convex line 15
2. theorem OAI.ScalarConductivity.periodic_pure_mode_family_correction line 22
3. lemma OAI.ScalarConductivity.flatPhaseMode_angularPeriodic line 114
4. lemma OAI.ScalarConductivity.flatFourier_angularPeriodic line 127
5. lemma OAI.ScalarConductivity.compactifiedFourierTail_angularPeriodic line 135
6. lemma OAI.ScalarConductivity.exists_normalized_periodic_end_cutoff line 146
7. theorem OAI.ScalarConductivity.exists_smooth_periodic_normalized_tail line 175