AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Generator

- The generator Dirichlet form `E(f,g) = integral f (-L)g d mu`.

noncomputable def dirichletForm
    (mu : Measure E) (generator : (E → ℝ) → E → ℝ)
    (f g : E → ℝ) : ℝ :=
  -(∫ x, f x * generator g x ∂mu)

/-- Variance as the squared centered `L2(mu)` norm. -/

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/Generator.lean:22published source at 77184245109a

- Variance as the squared centered `L2(mu)` norm.

noncomputable def variance (mu : Measure E) (f : E → ℝ) : ℝ :=
  ∫ x, (f x - ∫ y, f y ∂mu) ^ 2 ∂mu

/-- Domain conditions needed to read both sides of the generator Poincare
inequality as genuine finite integrals. -/

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/Generator.lean:28published source at 77184245109a

- Domain conditions needed to read both sides of the generator Poincare inequality as genuine finite integrals.

def PoincareAdmissible
    (mu : Measure E) (generator : (E → ℝ) → E → ℝ)
    (f : E → ℝ) : Prop :=
  Integrable f mu ∧
    Integrable (fun x => (f x - ∫ y, f y ∂mu) ^ 2) mu ∧
    Integrable (fun x => f x * generator f x) mu

/-- Chewi Definition 1.2.19: the generator Poincare inequality
`Var_mu(f) <= C * E(f,f)` for every admissible observable. -/

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/Generator.lean:33published source at 77184245109a

- Chewi Definition 1.2.19: the generator Poincare inequality `Var_mu(f) <= C * E(f,f)` for every admissible observable.

def SatisfiesPoincare
    (mu : Measure E) (generator : (E → ℝ) → E → ℝ)
    (C : ℝ) : Prop :=
  IsProbabilityMeasure mu ∧ 0 < C ∧
    ∀ f : E → ℝ, PoincareAdmissible mu generator f →
      variance mu f ≤ C * dirichletForm mu generator f f

/-- Relative entropy of a density `rho` with respect to its reference
probability measure.  Mathlib's totalized `Real.log 0 = 0` gives the standard
zero-density convention in the product `rho * log rho`. -/

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/Generator.lean:42published source at 77184245109aOpen detailed card

- Relative entropy of a density `rho` with respect to its reference probability measure. Mathlib's totalized `Real.log 0 = 0` gives the standard zero-density convention in the product `rho * log rho`.

noncomputable def densityEntropy (mu : Measure E) (rho : E → ℝ) : ℝ :=
  ∫ x, rho x * Real.log (rho x) ∂mu

/-- Domain conditions for the density formulation of log-Sobolev. -/

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/Generator.lean:52published source at 77184245109a

- Domain conditions for the density formulation of log-Sobolev.

def LogSobolevAdmissible
    (mu : Measure E) (generator : (E → ℝ) → E → ℝ)
    (rho : E → ℝ) : Prop :=
  (0 ≤ rho) ∧
    Integrable rho mu ∧
    (∫ x, rho x ∂mu) = 1 ∧
    Integrable (fun x => rho x * Real.log (rho x)) mu ∧
    Integrable (fun x => rho x * generator (fun y => Real.log (rho y)) x) mu

/-- Chewi Definition 1.2.25: the density log-Sobolev inequality
`KL(rho mu || mu) <= (C/2) E(rho, log rho)`. -/

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/Generator.lean:56published source at 77184245109a

- Chewi Definition 1.2.25: the density log-Sobolev inequality `KL(rho mu || mu) <= (C/2) E(rho, log rho)`.

def SatisfiesLogSobolev
    (mu : Measure E) (generator : (E → ℝ) → E → ℝ)
    (C : ℝ) : Prop :=
  IsProbabilityMeasure mu ∧ 0 < C ∧
    ∀ rho : E → ℝ, LogSobolevAdmissible mu generator rho →
      densityEntropy mu rho ≤
        (C / 2) * dirichletForm mu generator rho (fun x => Real.log (rho x))

end Generator
end FunctionalInequalities
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/Generator.lean:67published source at 77184245109aOpen detailed card