Model.lean`

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.IndependentProducts.Vertex line 15
Source documentation
The tree of finite sequences of positive integers.
Also declared: ComparatorChallenges/IndependentProducts.lean:15 (same declaration text).
```
abbrev Vertex := List ℕ+
```
abbrev OAI.IndependentProducts.Edge line 17
Source documentation
Coordinates are attached only to nonroot vertices.
Also declared: ComparatorChallenges/IndependentProducts.lean:17 (same declaration text).
```
abbrev Edge := {v : Vertex // v ≠ []}
```
Mentions: OAI.IndependentProducts.Vertex
abbrev OAI.IndependentProducts.Sample line 18
Also declared: ComparatorChallenges/IndependentProducts.lean:18 (same declaration text).
def OAI.IndependentProducts.productMeasure line 21
Source documentation
The product law of independent copies of the multiplier.
Also declared: ComparatorChallenges/IndependentProducts.lean:21 (same declaration text).
```
def productMeasure (μ : Measure ℝ) : Measure Sample :=
…
```
Mentions: OAI.IndependentProducts.Sample
def OAI.IndependentProducts.pathPrefix line 25
Source documentation
The nonroot prefix ending at position j.
Also declared: ComparatorChallenges/IndependentProducts.lean:25 (same declaration text).
```
def pathPrefix (v : Vertex) (j : Fin v.length) : Edge :=
…
```
Mentions: OAI.IndependentProducts.Vertex, OAI.IndependentProducts.Edge
def OAI.IndependentProducts.pathProduct line 34
Source documentation
Root product is the empty product 1; every other product uses the path prefixes.
Also declared: ComparatorChallenges/IndependentProducts.lean:34 (same declaration text).
```
def pathProduct (v : Vertex) (ω : Sample) : ℝ :=
…
```
Mentions: OAI.IndependentProducts.Vertex, OAI.IndependentProducts.Sample
def OAI.IndependentProducts.productSpan line 38
Source documentation
The closed real L1 span of the path products.
Also declared: ComparatorChallenges/IndependentProducts.lean:38 (same declaration text).
```
def productSpan (μ : Measure ℝ) : Submodule ℝ (Lp ℝ 1 (productMeasure μ)) :=
…
```
Mentions: OAI.IndependentProducts.productMeasure
structure OAI.IndependentProducts.MultiplierHypotheses line 43
Source documentation
Positivity, nonconstancy, mean one, and finite second moment of the multiplier law.
Distinct definitions of this name: ComparatorChallenges/IndependentProducts.lean:43 (same statement text; different proof or body). Qualify references as OAI.IndependentProducts.MultiplierHypotheses@path.
```
structure MultiplierHypotheses (μ : Measure ℝ) : Prop where
…
```
def OAI.IndependentProducts.CofiniteSubspaces line 55
Source documentation
Closed subspaces of finite codimension, with respect to the inherited topology.
Also declared: ComparatorChallenges/IndependentProducts.lean:53 (same declaration text).
```
def CofiniteSubspaces : Set (Submodule ℝ X) :=
…
```
def OAI.IndependentProducts.averagedMidpointModulus line 59
Source documentation
The averaged asymptotic midpoint modulus, with directions of norm at least 1.
Also declared: ComparatorChallenges/IndependentProducts.lean:57 (same declaration text).
```
def averagedMidpointModulus (N : Seminorm ℝ X) (t : ℝ) : ℝ :=
…
```
def OAI.IndependentProducts.oneSidedModulus line 66
Source documentation
The usual one-sided modulus, whose directions have norm exactly 1.
Also declared: ComparatorChallenges/IndependentProducts.lean:64 (same declaration text).
```
def oneSidedModulus (N : Seminorm ℝ X) (t : ℝ) : ℝ :=
…
```
def OAI.IndependentProducts.IsEquivalentNorm line 72
Source documentation
A seminorm with these bounds is a genuine norm equivalent to the original norm.
Also declared: ComparatorChallenges/IndependentProducts.lean:70 (same declaration text).
```
def IsEquivalentNorm (N : Seminorm ℝ X) : Prop :=
…
```
def OAI.IndependentProducts.IsAUC line 75
Also declared: ComparatorChallenges/IndependentProducts.lean:73 (same declaration text).
def OAI.IndependentProducts.gaussianTail line 80
Source documentation
Gaussian-tail probability, in real rather than extended-nonnegative-real notation.
Also declared: ComparatorChallenges/IndependentProducts.lean:76 (same declaration text).
```
def gaussianTail (r : ℝ) : ℝ :=
…
```
def OAI.IndependentProducts.excessConstant line 84
Source documentation
The Gaussian excess constant at threshold twice the parameter.
Also declared: ComparatorChallenges/IndependentProducts.lean:80 (same declaration text).
```
def excessConstant (K : ℝ) : ℝ :=
…
```
def OAI.IndependentProducts.exponentialLaw line 88
Source documentation
The density exp(-w) on the positive half-line.
Also declared: ComparatorChallenges/IndependentProducts.lean:84 (same declaration text).
```
def exponentialLaw : Measure ℝ := expMeasure 1
```
def OAI.IndependentProducts.gaussianSquareLaw line 91
Source documentation
The law of the square of a standard real Gaussian.
Also declared: ComparatorChallenges/IndependentProducts.lean:87 (same declaration text).
```
def gaussianSquareLaw : Measure ℝ := (gaussianReal 0 1).map (fun x : ℝ => x ^ 2)
…
```