IndisputableMonolith.Papers.GCIC.ReducedPhasePotential

declarations in this module (16)

• def distZ L37
• theorem distZ_nonneg L40
• theorem distZ_le_half L44
• theorem distZ_add_int L52
• theorem distZ_periodic L57
• theorem distZ_eq_zero_iff L63
• def Jtilde L82
• theorem Jtilde_nonneg L86
• theorem Jtilde_periodic L91
• theorem Jtilde_add_int L96
• lemma cosh_eq_one_iff L102
• theorem Jtilde_zero_iff L110
• theorem Jtilde_stiffness_lb L133
• def gcic_kappa L139
• theorem gcic_kappa_pos L141
• theorem phase_rigidity L155