`BookProof.CarlemanUnboundedHop.kernelOp_deficiencyTrivialAt` {a : ℕ → ℕ → ℂ} {A θ Θ : ℕ → ℝ} (hk : IsL2Kernel a) (hθ0 : ∀ r, 0 ≤ θ r) (hΘ : ∀ j, HasSum (fun i => θ (i...

Proved

BookProof.CarlemanUnboundedHop.kernelOp_deficiencyTrivialAt

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterCarlemanUnboundedHop.

BookProof.CarlemanUnboundedHop.kernelOp_deficiencyTrivialAt {a : ℕ → ℕ → ℂ} {A θ Θ : ℕ → ℝ} (hk : IsL2Kernel a) (hθ0 : ∀ r, 0 ≤ θ r) (hΘ : ∀ j, HasSum (fun i => θ (i + j + 1)) (Θ j)) (hΘsum : Summable Θ) (hApos : ∀ n, 0 < A n) (hAmono : Monotone A) (hbd : ∀ n k, n < k → ‖a n k‖ ≤ A n * θ (k - n)) (hcar : ¬ Summable fun n => (A n)⁻¹) {z : ℂ} (hz : z.im ≠ 0) : DeficiencyTrivialAt (lpFiniteModes ℕ) (kernelOp hk) z

Formalization note: Lean 4 identifier BookProof.CarlemanUnboundedHop.kernelOp_deficiencyTrivialAt.

Preamble

-- Generated from ChapterCarlemanUnboundedHop.lean — theorem BookProof.CarlemanUnboundedHop.kernelOp_deficiencyTrivialAt
import Mathlib
import Definitions.Def_ChapterCarlemanUnboundedHop
import Definitions.Def_ChapterFarisLavineCore
import Definitions.Def_ChapterKernelBound
import Definitions.Def_ChapterNavierStokesEsa
open BookProof.KernelBound
open BookProof.CarlemanUnboundedHop



open Finset
open BookProof.FarisLavine
open BookProof.NavierStokesFlow

noncomputable section

variable {a : ℕ → ℕ → ℂ} {u : ℕ → ℂ} {A θ Θ : ℕ → ℝ}

Formal statement

theorem BookProof.CarlemanUnboundedHop.kernelOp_deficiencyTrivialAt {a : ℕ → ℕ → ℂ} {A θ Θ : ℕ → ℝ} (hk : IsL2Kernel a)
    (hθ0 : ∀ r, 0 ≤ θ r) (hΘ : ∀ j, HasSum (fun i => θ (i + j + 1)) (Θ j))
    (hΘsum : Summable Θ) (hApos : ∀ n, 0 < A n) (hAmono : Monotone A)
    (hbd : ∀ n k, n < k → ‖a n k‖ ≤ A n * θ (k - n))
    (hcar : ¬ Summable fun n => (A n)⁻¹) {z : ℂ} (hz : z.im ≠ 0) :
    DeficiencyTrivialAt (lpFiniteModes ℕ) (kernelOp hk) z := by sorry

View graph