`BookProof.NavierStokesFlow.AffineBlock.affBlockH_not_bounded` (κ c : J → ℝ) (hκ : ∀ j, 0 ≤ κ j) (hc : ∀ j, 0 ≤ c j) (hunb : ∀ C : ℝ, ∃ j, C < κ j) (C : ℝ) : ∃ x :...

Proved

BookProof.NavierStokesFlow.AffineBlock.affBlockH_not_bounded

by leonardopedro · Oct 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterNavierStokesAffineBlockEsa.

BookProof.NavierStokesFlow.AffineBlock.affBlockH_not_bounded (κ c : J → ℝ) (hκ : ∀ j, 0 ≤ κ j) (hc : ∀ j, 0 ≤ c j) (hunb : ∀ C : ℝ, ∃ j, C < κ j) (C : ℝ) : ∃ x : lpFiniteModes (ℕ × J), ‖((x : lpFiniteModes (ℕ × J)) : L2I (ℕ × J))‖ = 1 ∧ C < ‖affBlockH κ c hκ hc x‖

Formalization note: Lean 4 identifier BookProof.NavierStokesFlow.AffineBlock.affBlockH_not_bounded.

Preamble

-- Generated from ChapterNavierStokesAffineBlockEsa.lean — theorem BookProof.NavierStokesFlow.AffineBlock.affBlockH_not_bounded
import Mathlib
import Definitions.Def_ChapterNavierStokesAffineBlockEsa
import Definitions.Def_ChapterNavierStokesAffineFiberEsa
import Definitions.Def_ChapterNavierStokesEsa
import Definitions.Def_ChapterNavierStokesHermiteFarisLavine
import Definitions.Def_ChapterNavierStokesIkebeKato
import Definitions.Def_ChapterStoneResolvent
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow.AffineFiber.PairShift
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow.AffineBlock


open scoped ENNReal



open LpNat BookProof.FarisLavine IkebeKato HermiteFarisLavine ShiftHamiltonian AffineFiber BilinearEsa

variable {J : Type*}

Formal statement

theorem BookProof.NavierStokesFlow.AffineBlock.affBlockH_not_bounded (κ c : J → ℝ) (hκ : ∀ j, 0 ≤ κ j) (hc : ∀ j, 0 ≤ c j)
    (hunb : ∀ C : ℝ, ∃ j, C < κ j) (C : ℝ) :
    ∃ x : lpFiniteModes (ℕ × J),
      ‖((x : lpFiniteModes (ℕ × J)) : L2I (ℕ × J))‖ = 1
        ∧ C < ‖affBlockH κ c hκ hc x‖ := by sorry

View graph