OAI/Analysis/Mahler/PlanarSymmetry.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SymmetricMahler.inverseF_deriv_conj line 10
2. lemma OAI.SymmetricMahler.planarDensity_conj line 23
3. theorem OAI.SymmetricMahler.planarPrimitive_neg line 30

   Source documentation

   Conjugation changes the sign of the original vertical primitive.

   theorem planarPrimitive_neg (m : ℕ) {q t : ℝ}
       (hseg : ∀ s ∈ uIcc (0 : ℝ) t, (q : ℂ)+(s : ℂ)*Complex.I ∈ MahlerConformal.Omega) :
       planarPrimitive m q (-t) = -planarPrimitive m q t := by
   …

   Mentions: OAI.MahlerConformal.Omega, OAI.SymmetricMahler.planarPrimitive