OAI/NumberTheory/PiExponent/Approximation/WeightedSectionOrder.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.WeightedSectionOrder.coefficient_tilde_end line 17
2. def OAI.PiExponent.WeightedSectionOrder.coordinateBasis line 35
3. def OAI.PiExponent.WeightedSectionOrder.coordinateFrame line 41
4. theorem OAI.PiExponent.WeightedSectionOrder.coordinate_coefficient line 47
5. theorem OAI.PiExponent.WeightedSectionOrder.coordinate_coefficient_image line 62
6. theorem OAI.PiExponent.WeightedSectionOrder.coordinate_coefficient_ne_zero line 75
7. def OAI.PiExponent.WeightedSectionOrder.sectionZeroEuler line 84
8. theorem OAI.PiExponent.WeightedSectionOrder.coordinate_zero_euler_eq_order_difference line 91
9. theorem OAI.PiExponent.WeightedSectionOrder.exists_constant_section_zero_euler_eq_weighted_pole line 116