Cumulant energies and localization drift terms

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Cumulant_Leibniz
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Operator_InverseSqrt

noncomputable section
open MeasureTheory
open FunctionalInequalities.Analysis FunctionalInequalities.Analysis.BakryEmery
open scoped RealInnerProductSpace
namespace FunctionalInequalities
namespace KLS
namespace BKL
variable {n : ℕ}
/-- The middle term `L_m` of BKL arXiv:2610.05474v1, (72), at a fixed law `ν` with covariance `A`:
`L_m(h) = Σ_{J ∋ i₀, 2 ≤ |J|, |Jᶜ| ≥ 2} ⟪κ_{|J|+1}(h_J, ·), A⁻¹ κ_{m−|J|+1}(h_{Jᶜ}, ·)⟫` (slot `i₀ = 0`). -/
def lowerDrift (ν : Measure (EuclideanSpace ℝ (Fin n))) {m : ℕ} (h : Fin m → EuclideanSpace ℝ (Fin n))
    (i₀ : Fin m) : ℝ :=
  ∑ q ∈ Finset.univ.filter (fun q : Fin m → Bool =>
      q i₀ = true ∧ 2 ≤ (selected h q).length ∧ 2 ≤ (selected h (fun i => !(q i))).length),
    ⟪cumulantVector ν (selected h q),
      Ring.inverse (Covariance.operator ν) (cumulantVector ν (selected h (fun i => !(q i))))⟫
/-- The cumulant energy `E_{r+1} = |κ_{r+1}(u)|²_A = Σ_J κ_{r+1}(u, σ e_{J_1}, …, σ e_{J_r})²`, `σ = A^{-1/2}`
(BKL (75)–(76)). -/
def cumulantEnergy (ν : Measure (EuclideanSpace ℝ (Fin n))) (r : ℕ) (u : EuclideanSpace ℝ (Fin n)) : ℝ :=
  ∑ J : Fin r → Fin n, cumulant ν (r + 1)
    (Fin.cons u fun k => inverseSqrt (Covariance.operator ν) (EuclideanSpace.basisFun (Fin n) ℝ (J k))) ^ 2
end BKL
end KLS
end FunctionalInequalities
section S4Section6Pointwise
open MeasureTheory
open FunctionalInequalities.Analysis FunctionalInequalities.Analysis.BakryEmery
open scoped RealInnerProductSpace
namespace FunctionalInequalities
namespace KLS
namespace BKL
variable {n : ℕ}
section Masks
/-- number of selected slots -/
def maskCount {k : ℕ} (q : Fin k → Bool) : ℕ := (Finset.univ.filter fun i => q i = true).card
end Masks
section Algebra
/-- `σ e_j` -/
def sigmaBasis (ν : Measure (EuclideanSpace ℝ (Fin n))) (j : Fin n) : EuclideanSpace ℝ (Fin n) :=
  inverseSqrt (Covariance.operator ν) (EuclideanSpace.basisFun (Fin n) ℝ j)
/-- One mask summand of `lowerDrift`. -/
def maskTerm (ν : Measure (EuclideanSpace ℝ (Fin n))) {m : ℕ} (h : Fin m → EuclideanSpace ℝ (Fin n))
    (q : Fin m → Bool) : ℝ :=
  ⟪cumulantVector ν (selected h q),
    Ring.inverse (Covariance.operator ν) (cumulantVector ν (selected h (fun i => !(q i))))⟫
/-- The masks of the middle allocations: slot `0` selected, at least two slots on each side. -/
def middleMasks (k : ℕ) : Finset (Fin (k + 1) → Bool) :=
  Finset.univ.filter fun q => q 0 = true ∧ 2 ≤ maskCount q ∧ 2 ≤ maskCount (fun i => !(q i))
/-- The squared pair term `⟪κ(u, l₁, ·), A⁻¹ κ(l₂, ·)⟫²` as a function of the two selected lists. -/
def pairTerm (ν : Measure (EuclideanSpace ℝ (Fin n))) (u : EuclideanSpace ℝ (Fin n))
    (l₁ l₂ : List (EuclideanSpace ℝ (Fin n))) : ℝ :=
  ⟪cumulantVector ν (u :: l₁), Ring.inverse (Covariance.operator ν) (cumulantVector ν l₂)⟫ ^ 2
end Algebra
end BKL
end KLS
end FunctionalInequalities
end S4Section6Pointwise