Model.lean`

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.LogConcaveSampling.Point line 16
Also declared: ComparatorChallenges/LogConcaveQuery.lean:12 (same declaration text).
abbrev OAI.LogConcaveSampling.Reply line 17
Also declared: ComparatorChallenges/LogConcaveQuery.lean:13 (same declaration text).
abbrev OAI.LogConcaveSampling.Transcript line 18
Also declared: ComparatorChallenges/LogConcaveQuery.lean:14 (same declaration text).
structure OAI.LogConcaveSampling.Admissible line 21
Source documentation
Normalized twice continuously differentiable potentials with Hessian between the identity and twice the identity.
Also declared: ComparatorChallenges/LogConcaveQuery.lean:17 (same declaration text).
```
structure Admissible {d : ℕ} (V : Point d → ℝ) : Prop where
…
```
Mentions: OAI.LogConcaveSampling.Point
def OAI.LogConcaveSampling.gibbsDensity line 30
Source documentation
The unnormalized Gibbs density relative to Euclidean volume.
Also declared: ComparatorChallenges/LogConcaveQuery.lean:26 (same declaration text).
```
def gibbsDensity {d : ℕ} (V : Point d → ℝ) (x : Point d) : ℝ≥0∞ :=
…
```
Mentions: OAI.LogConcaveSampling.Point
def OAI.LogConcaveSampling.partition line 33
Also declared: ComparatorChallenges/LogConcaveQuery.lean:29 (same declaration text).
def OAI.LogConcaveSampling.gibbs line 37
Source documentation
The Gibbs probability law, normalized by its partition function.
Also declared: ComparatorChallenges/LogConcaveQuery.lean:33 (same declaration text).
```
def gibbs {d : ℕ} (V : Point d → ℝ) : Measure (Point d) :=
…
```
Mentions: OAI.LogConcaveSampling.Point
def OAI.LogConcaveSampling.TVAtMost line 40
Also declared: ComparatorChallenges/LogConcaveQuery.lean:36 (same declaration text).
def OAI.LogConcaveSampling.firstOrderReply line 44
Also declared: ComparatorChallenges/LogConcaveQuery.lean:40 (same declaration text).
structure OAI.LogConcaveSampling.OracleAlgorithm line 48
Source documentation
Measurable adaptive queries and output, parametrized by private randomness.
Also declared: ComparatorChallenges/LogConcaveQuery.lean:44 (same declaration text).
```
structure OracleAlgorithm (Ω : Type*) [MeasurableSpace Ω] (d q : ℕ) where
…
```
def OAI.LogConcaveSampling.OracleAlgorithm.history line 54
Also declared: ComparatorChallenges/LogConcaveQuery.lean:50 (same declaration text).
def OAI.LogConcaveSampling.OracleAlgorithm.run line 63
Also declared: ComparatorChallenges/LogConcaveQuery.lean:59 (same declaration text).
def OAI.LogConcaveSampling.CanSample line 68
Source documentation
A uniform sampler with a deterministic query budget on every execution and total-variation error at most one tenth.
Also declared: ComparatorChallenges/LogConcaveQuery.lean:64 (same declaration text).
```
def CanSample (d q : ℕ) : Prop :=
…
```
def OAI.LogConcaveSampling.queryComplexity line 75
Source documentation
The smallest feasible integer query budget, or infinity when no budget is feasible.
Also declared: ComparatorChallenges/LogConcaveQuery.lean:71 (same declaration text).
```
def queryComplexity (d : ℕ) : ℕ∞ :=
…
```
def OAI.LogConcaveSampling.ExponentBound line 79
Source documentation
The quantified dimension-exponent upper bound with every positive exponent slack.
Also declared: ComparatorChallenges/LogConcaveQuery.lean:75 (same declaration text).
```
def ExponentBound (γ : ℝ) : Prop :=
…
```
def OAI.LogConcaveSampling.gammaStar line 83
Also declared: ComparatorChallenges/LogConcaveQuery.lean:79 (same declaration text).