{g₁ g₂ : ℝ} (h0 : 0 ≤ g₁) (h : g₁ < g₂) : strongCoupling g₁ < strongCoupling g₂
ProvedBookProof.SirkGapTable.strongCoupling_ltsirkspectral-theorytimepiece
Lean 4 theorem BookProof.SirkGapTable.strongCoupling_lt (module BookProof.SirkGapTable), source chapter BookProof/ChapterSirkGapTable.lean.
Preamble
-- Generated from ChapterSirkGapTable.lean — theorem BookProof.SirkGapTable.strongCoupling_lt
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]Formal statement
theorem BookProof.SirkGapTable.strongCoupling_lt {g₁ g₂ : ℝ} (h0 : 0 ≤ g₁) (h : g₁ < g₂) :
strongCoupling g₁ < strongCoupling g₂ := by sorrySource