OAI/Combinatorics/SharpThreshold/NoiseKernel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem313.NoiseKernel.spectral_kernel line 17

   Source documentation

   The subset-indexed spectral kernel factors coordinatewise.

   theorem spectral_kernel (ρ : ℝ) (φ : ι → α → ℝ) (x y : α) :
       (∑ S : Finset ι, ρ ^ S.card * (∏ i ∈ S, φ i x) * (∏ i ∈ S, φ i y)) =
         ∏ i, (1 + ρ * φ i x * φ i y) := by
   …

2. theorem OAI.Problem313.NoiseKernel.spectral_eq_kernel line 30

   Source documentation

   A spectral multiplier by ρ ^ |S| is the corresponding weighted product-kernel operator. No orthogonality hypotheses are needed for this algebraic identity.

   theorem spectral_eq_kernel (ρ : ℝ) (φ : ι → α → ℝ) (w g : α → ℝ) (x : α) :
       (∑ S : Finset ι, ρ ^ S.card *
         (∑ y, w y * g y * (∏ i ∈ S, φ i y)) * (∏ i ∈ S, φ i x)) =
       ∑ y, w y * g y * ∏ i, (1 + ρ * φ i x * φ i y) := by
   …