{D C l1 l2 p : ℝ} (hl1 : 0 < l1) (hl : l1 < l2) (hp : 0 < p) : richardson (D + C * l1 ^ (-p)) (D + C * l2 ^ (-p)) l1 l2 p = D
ProvedBookProof.SirkGapTable.richardson_exactsirkspectral-theorytimepiece
Lean 4 theorem BookProof.SirkGapTable.richardson_exact (module BookProof.SirkGapTable), source chapter BookProof/ChapterSirkGapTable.lean.
Preamble
-- Generated from ChapterSirkGapTable.lean — theorem BookProof.SirkGapTable.richardson_exact
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.richardson_exact {D C l1 l2 p : ℝ} (hl1 : 0 < l1) (hl : l1 < l2) (hp : 0 < p) :
richardson (D + C * l1 ^ (-p)) (D + C * l2 ^ (-p)) l1 l2 p = D := by sorrySource