`BookProof.ChapterFreeFieldBornSurj.bornSection_apply` (p : Fin n → ℝ) (k : Fin n) : bornSection p k = Real.sqrt (p k)

Proved

BookProof.ChapterFreeFieldBornSurj.bornSection_apply

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterFreeFieldBornSurj.

BookProof.ChapterFreeFieldBornSurj.bornSection_apply (p : Fin n → ℝ) (k : Fin n) : bornSection p k = Real.sqrt (p k)

Formalization note: Lean 4 identifier BookProof.ChapterFreeFieldBornSurj.bornSection_apply.

Preamble

-- Generated from ChapterFreeFieldBornSurj.lean — theorem BookProof.ChapterFreeFieldBornSurj.bornSection_apply
import Definitions.Def_ChapterFreeFieldGaussian
import Definitions.Def_ChapterFreeFieldSphere
import Definitions.Def_ChapterFreeFieldSphereSupport
import Definitions.Def_ChapterFreeFieldBorn
import Mathlib
import Definitions.Def_ChapterFreeFieldBornSurj
open BookProof.ChapterFreeFieldBornSurj

variable {n : ℕ}


open MeasureTheory
open BookProof.ChapterFreeFieldGaussian BookProof.ChapterFreeFieldSphere
open BookProof.ChapterFreeFieldSphereSupport BookProof.ChapterFreeFieldBorn

Formal statement

theorem BookProof.ChapterFreeFieldBornSurj.bornSection_apply (p : Fin n → ℝ) (k : Fin n) :
    bornSection p k = Real.sqrt (p k) := by sorry

View graph