theorem proved term proof

`zero_composition_diverges`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 192theorem zero_composition_diverges (ρ : ℂ) (hρ : ¬OnCriticalLine ρ) (C : ℝ) :
 193    ∃ n : ℕ, C < defectIterate (zeroDeviation ρ) n := by

proof body

Term-mode proof.

 194  apply defectIterate_unbounded
 195  exact (zeroDeviation_eq_zero_iff_on_critical_line ρ).not.mpr hρ
 196
 197end
 198
 199end NumberTheory
 200end IndisputableMonolith

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

composition_violates_budget in IndisputableMonolith.NumberTheory.CompositionDivergence decl_use

depends on (5)

Lean names referenced from this declaration's body.

defectIterate in IndisputableMonolith.NumberTheory.ZeroCompositionLaw decl_use
defectIterate_unbounded in IndisputableMonolith.NumberTheory.ZeroCompositionLaw decl_use
OnCriticalLine in IndisputableMonolith.NumberTheory.ZeroLocationCost decl_use
zeroDeviation in IndisputableMonolith.NumberTheory.ZeroLocationCost decl_use
zeroDeviation_eq_zero_iff_on_critical_line in IndisputableMonolith.NumberTheory.ZeroLocationCost decl_use