{l1 l2 p : ℝ} (hl1 : 0 < l1) (hl : l1 < l2) (hp : 0 < p) : 1 < (l2 / l1) ^ p
ProvedBookProof.SirkGapTable.one_lt_ratiosirkspectral-theorytimepiece
Lean 4 theorem BookProof.SirkGapTable.one_lt_ratio (module BookProof.SirkGapTable), source chapter BookProof/ChapterSirkGapTable.lean.
Preamble
-- Generated from ChapterSirkGapTable.lean — theorem BookProof.SirkGapTable.one_lt_ratio
import Mathlib
import Definitions.Def_ChapterSirkGapTable
open BookProof.SirkGapTable
noncomputable section
open BookProof.SirkCertifiedGap
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]
open RealFormal statement
theorem BookProof.SirkGapTable.one_lt_ratio {l1 l2 p : ℝ} (hl1 : 0 < l1) (hl : l1 < l2) (hp : 0 < p) :
1 < (l2 / l1) ^ p := by sorrySource