Prove2Me

`BookProof.ChapterF3.overlap_prod_pos` {ι : Type*} (s : Finset ι) (w : ι → ℝ) (hw : ∀ i ∈ s, 0 < w i) : 0 < ∏ i ∈ s, Real.sqrt (w i / (2 * Real.pi))

Proved
BookProof.ChapterF3.overlap_prod_pos

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterF3.

BookProof.ChapterF3.overlap_prod_pos {ι : Type*} (s : Finset ι) (w : ι → ℝ) (hw : ∀ i ∈ s, 0 < w i) : 0 < ∏ i ∈ s, Real.sqrt (w i / (2 * Real.pi))

Formalization note: Lean 4 identifier BookProof.ChapterF3.overlap_prod_pos.

Preamble
-- Generated from ChapterF3.lean — theorem BookProof.ChapterF3.overlap_prod_pos
import Mathlib
import Definitions.Def_ChapterF3
open BookProof.ChapterF3


open scoped BigOperators
open Polynomial


noncomputable section

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]
Formal statement
theorem BookProof.ChapterF3.overlap_prod_pos {ι : Type*} (s : Finset ι) (w : ι → ℝ) (hw : ∀ i ∈ s, 0 < w i) :
    0 < ∏ i ∈ s, Real.sqrt (w i / (2 * Real.pi)) := by sorry

View graph