277structure RecognitionThetaModularIdentity : Prop where 278 prefactor : ∃ ρ : ℝ → ℝ, Continuous ρ ∧ 279 ∀ t : ℝ, 0 < t → 280 recognitionTheta (1 / t) = ρ t * recognitionTheta t 281 282/-- Sub-conjecture A.3: the Mellin transform of `Θ̃_RS` factors as 283 `ζ(s) · G_RS(s)` where `G_RS` is a meromorphic function inheriting 284 the reflection symmetry from the modular identity. 285 286 We package the existence of the factorization as a Prop. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.