OAI/NumberTheory/EgyptianFractions/ReciprocalPhaseVariation.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem337.ReciprocalPhase.phase line 9
  2. def OAI.Problem337.ReciprocalPhase.inversePhase line 11
  3. lemma OAI.Problem337.ReciprocalPhase.phase_re line 13
  4. lemma OAI.Problem337.ReciprocalPhase.phase_im line 18
  5. lemma OAI.Problem337.ReciprocalPhase.phase_normSq line 21
  6. lemma OAI.Problem337.ReciprocalPhase.inversePhase_re line 27
  7. lemma OAI.Problem337.ReciprocalPhase.inversePhase_im line 33
  8. lemma OAI.Problem337.ReciprocalPhase.phase_norm line 39
  9. lemma OAI.Problem337.ReciprocalPhase.inversePhase_norm line 45
  10. lemma OAI.Problem337.ReciprocalPhase.strictAntiOn_cot line 49
  11. lemma OAI.Problem337.ReciprocalPhase.inversePhase_im_strictMonoOn line 60
  12. lemma OAI.Problem337.ReciprocalPhase.sin_pi_mul_lower line 69
  13. lemma OAI.Problem337.ReciprocalPhase.inversePhase_norm_le line 86
  14. lemma OAI.Problem337.ReciprocalPhase.inversePhase_scaled_re line 94
  15. lemma OAI.Problem337.ReciprocalPhase.inversePhase_scaled_im_strictMonoOn line 102
  16. lemma OAI.Problem337.ReciprocalPhase.phase_ne_zero line 114
  17. def OAI.Problem337.ReciprocalPhase.unitPhase line 122

    Source documentation

    The unit-modulus exponential used in the first-derivative sum.

    def unitPhase (θ : ℝ) : ℂ := Complex.exp ((2 * θ : ℝ) * Complex.I)
  18. lemma OAI.Problem337.ReciprocalPhase.unitPhase_add line 124
  19. lemma OAI.Problem337.ReciprocalPhase.norm_unitPhase line 130
  20. lemma OAI.Problem337.ReciprocalPhase.inversePhase_mul_increment line 133
  21. lemma OAI.Problem337.ReciprocalPhase.inversePhase_norm_sub line 143