The Lean 4 theorem `diagKR_drift_not_bounded` in the `ChapterNavierStokesLagrangianKatoRellich` chapter of the timepiece formalization
ProvedBookProof.NavierStokesFlow.LagrangianKatoRellich.diagKR_drift_not_boundedtimepiece
The Lean 4 theorem diagKR_drift_not_bounded in the ChapterNavierStokesLagrangianKatoRellich chapter of the timepiece formalization.
Preamble
-- Generated from ChapterNavierStokesLagrangianKatoRellich.lean — theorem BookProof.NavierStokesFlow.LagrangianKatoRellich.diagKR_drift_not_bounded
import Mathlib
import Definitions.Def_ChapterNavierStokesLagrangianKatoRellich
import Definitions.Def_ChapterSirkBandLedger
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow.LagrangianKatoRellich
open Filter Topology
open BookProof.NavierStokesFlow.FullEsa BookProof.NavierStokesFlow.LagrangianEsa BookProof.FarisLavine
open BookProof.EsaClosure BookProof.HashimotoShiftInvert BookProof.HermiteGalerkin
variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F]
variable (L : LagrangianFullData F)
variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]
variable (L : LagrangianFullData F)
open BookProof.NavierStokesFlow.LpNat BookProof.NavierStokesFlow.DiagonalEsaFormal statement
theorem BookProof.NavierStokesFlow.LagrangianKatoRellich.diagKR_drift_not_bounded :
¬ ∃ C : ℝ, ∀ f : diagKR.D, ‖diagKR.drift f‖ ≤ C * ‖f‖ := by sorrySource