structure
definition
ClassicalZeroFreeRegionAttackSurface
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.ClassicalZeroFreeRegion on GitHub at line 88.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
85/-- Machine-readable Track B1 status. The elementary positivity kernel is
86proved; the remaining field is exactly the classical analytic zero-free-region
87input. -/
88structure ClassicalZeroFreeRegionAttackSurface where
89 trig_kernel_nonneg :
90 ∀ θ : ℝ, 0 ≤ 3 + 4 * Real.cos θ + Real.cos (2 * θ)
91 open_deLaValleePoussin :
92 DeLaValleePoussinZeroFreeRegion → StripZeroFreeBridge
93
94def classicalZeroFreeRegionAttackSurface :
95 ClassicalZeroFreeRegionAttackSurface where
96 trig_kernel_nonneg := deLaValleePoussin_trig_kernel_nonneg
97 open_deLaValleePoussin := stripZeroFreeBridge_of_deLaValleePoussin
98
99end
100
101end ClassicalZeroFreeRegion
102end NumberTheory
103end IndisputableMonolith