`BookProof.FockInteractionStability.gap_persists_of_bounded_form` {q v : E → ℝ} {S : Set E} {mu b : ℝ} (hq : ∀ x ∈ S, mu * ‖x‖ ^ 2 ≤ q x) (hv : ∀ x, |v x| ≤ b * ‖x‖ ^ 2)...

Proved

BookProof.FockInteractionStability.gap_persists_of_bounded_form

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterFockInteractionStability.

BookProof.FockInteractionStability.gap_persists_of_bounded_form {q v : E → ℝ} {S : Set E} {mu b : ℝ} (hq : ∀ x ∈ S, mu * ‖x‖ ^ 2 ≤ q x) (hv : ∀ x, |v x| ≤ b * ‖x‖ ^ 2) : ∀ x ∈ S, (mu - b) * ‖x‖ ^ 2 ≤ q x + v x

Formalization note: Lean 4 identifier BookProof.FockInteractionStability.gap_persists_of_bounded_form.

Preamble

-- Generated from ChapterFockInteractionStability.lean — theorem BookProof.FockInteractionStability.gap_persists_of_bounded_form
import Definitions.Def_ChapterFockSecondQuantization
import Definitions.Def_ChapterFockOneParticleGap
import Definitions.Def_ChapterFockNumberPreservingGap
import Definitions.Def_ChapterFarisLavine
import Definitions.Def_ChapterNavierStokesAffineFiberEsa
import Mathlib
import Definitions.Def_ChapterFockInteractionStability
open BookProof.FockInteractionStability

variable {E : Type*} [NormedAddCommGroup E]


noncomputable section


open BookProof.FockSecondQuantization BookProof.FockOneParticleGap
open BookProof.FockNumberPreservingGap
open BookProof.FarisLavine BookProof.NavierStokesFlow

Formal statement

theorem BookProof.FockInteractionStability.gap_persists_of_bounded_form
    {q v : E → ℝ} {S : Set E} {mu b : ℝ}
    (hq : ∀ x ∈ S, mu * ‖x‖ ^ 2 ≤ q x)
    (hv : ∀ x, |v x| ≤ b * ‖x‖ ^ 2) :
    ∀ x ∈ S, (mu - b) * ‖x‖ ^ 2 ≤ q x + v x := by sorry

View graph