FiniteParseval.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite Parseval identities from a weighted kernel

The algebraic statement below separates finite-sum rearrangement from the concrete kernel identity. Neither the expansion nor the Parseval identity requires nonnegative weights.

theorem OAI.TalagrandDiscreteConvexity.weighted_transform_bilinear_expansion line 23

Source documentation

Expanding a weighted product of transforms gives the associated kernel.

theorem weighted_transform_bilinear_expansion
    (K : I → J → ℝ) (r : I → ℝ) (f g : J → ℝ) :
    (∑ u, r u * (∑ x, f x * K u x) * (∑ y, g y * K u y)) =
      ∑ x, ∑ y, f x * g y * (∑ u, r u * K u x * K u y) := by
…

theorem OAI.TalagrandDiscreteConvexity.weighted_kernel_bilinear line 49

Source documentation

A diagonal weighted kernel preserves the corresponding bilinear form.

theorem weighted_kernel_bilinear
    (K : I → J → ℝ) (r : I → ℝ) (μ : J → ℝ)
    (hkernel : ∀ x y, (∑ u, r u * K u x * K u y) =
      if x = y then μ x else 0) (f g : J → ℝ) :
    (∑ u, r u * (∑ x, f x * K u x) * (∑ y, g y * K u y)) =
      ∑ x, μ x * f x * g x := by
…

theorem OAI.TalagrandDiscreteConvexity.weighted_kernel_parseval line 70

Source documentation

Finite Parseval follows from the weighted kernel identity.

theorem weighted_kernel_parseval
    (K : I → J → ℝ) (r : I → ℝ) (μ : J → ℝ)
    (hkernel : ∀ x y, (∑ u, r u * K u x * K u y) =
      if x = y then μ x else 0) (f : J → ℝ) :
    (∑ u, r u * (∑ x, f x * K u x) ^ 2) =
      ∑ x, μ x * (f x) ^ 2 := by
…