No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
35theorem deLaValleePoussin_trig_kernel_eq_square (θ : ℝ) :
36 3 + 4 * Real.cos θ + Real.cos (2 * θ) =
37 2 * (Real.cos θ + 1) ^ 2 := by
proof body
Term-mode proof.
38 rw [Real.cos_two_mul]
39 ring
40
41/-- Positivity of the de la Vallee-Poussin trigonometric kernel. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (7)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
kernel
in IndisputableMonolith.Cosmology.BITKernelFamilies
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
kernel
in IndisputableMonolith.ILG.Kernel
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use