Model.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.LeanBlast.KLS.Space line 12
def OAI.LeanBlast.KLS.densityMeasure line 15
Source documentation
The ordinary Lebesgue-density measure.
```
def densityMeasure {n : ℕ} (ρ : Space n → ℝ) : Measure (Space n) :=
…
```
Mentions: OAI.LeanBlast.KLS.Space
structure OAI.LeanBlast.KLS.IsLogConcaveDensity line 20
Source documentation
Probability-density and log-concavity conditions. ConcaveOn includes convexity of the positive support.
```
structure IsLogConcaveDensity {n : ℕ} (ρ : Space n → ℝ) : Prop where
…
```
Mentions: OAI.LeanBlast.KLS.Space
structure OAI.LeanBlast.KLS.IsIsotropic line 27
Source documentation
Zero mean and identity covariance, with all moment integrability explicit.
```
structure IsIsotropic {n : ℕ} (μ : Measure (Space n)) : Prop where
…
```
Mentions: OAI.LeanBlast.KLS.Space
def OAI.LeanBlast.KLS.expectation line 34
def OAI.LeanBlast.KLS.variance line 37
def OAI.LeanBlast.KLS.dirichletEnergy line 40
def OAI.LeanBlast.KLS.IsTestFunction line 44
Source documentation
The exact compactly supported smooth real test-function class.
```
def IsTestFunction {n : ℕ} (f : Space n → ℝ) : Prop :=
…
```
Mentions: OAI.LeanBlast.KLS.Space
def OAI.LeanBlast.KLS.PoincareBound line 48
Source documentation
Direct Poincare inequality, avoiding an infimum convention for the constant.
```
def PoincareBound {n : ℕ} (μ : Measure (Space n)) (C : ℝ) : Prop :=
…
```
Mentions: OAI.LeanBlast.KLS.Space
def OAI.LeanBlast.KLS.KLSStatement line 53
Source documentation
The full dimension-free statement: one constant works for every dimension, every isotropic log-concave density, and every smooth compactly supported test.
```
def KLSStatement : Prop :=
…
```
abbrev OAI.LeanBlast.KLS.FullStatement line 58