Model.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.Bernoulli.Space line 14
Also declared: ComparatorChallenges/BernoulliNonflatInSeven.lean:13 (same declaration text).
def OAI.Bernoulli.Test line 17
Source documentation
Compactly supported smooth real tests in the open set.
Also declared: ComparatorChallenges/BernoulliNonflatInSeven.lean:16 (same declaration text).
```
def Test {d : ℕ} (D : Set (Space d)) (φ : Space d → ℝ) : Prop :=
…
```
Mentions: OAI.Bernoulli.Space
def OAI.Bernoulli.WeakGradient line 21
Source documentation
Distributional gradient, tested in every constant direction.
Also declared: ComparatorChallenges/BernoulliNonflatInSeven.lean:20 (same declaration text).
```
def WeakGradient {d : ℕ} (D : Set (Space d))
    (u : Space d → ℝ) (G : Space d → Space d) : Prop :=
…
```
Mentions: OAI.Bernoulli.Space
def OAI.Bernoulli.H1 line 28
Source documentation
H¹(D), with its weak gradient.
Also declared: ComparatorChallenges/BernoulliNonflatInSeven.lean:27 (same declaration text).
```
def H1 {d : ℕ} (D : Set (Space d))
    (u : Space d → ℝ) (G : Space d → Space d) : Prop :=
…
```
Mentions: OAI.Bernoulli.Space
def OAI.Bernoulli.H10 line 35
Source documentation
H¹₀(D) is H¹-closure of C∞ compactly supported functions. Both L² errors tend to zero. This does not restrict competitors to smooth ones.
Also declared: ComparatorChallenges/BernoulliNonflatInSeven.lean:34 (same declaration text).
```
def H10 {d : ℕ} (D : Set (Space d))
    (u : Space d → ℝ) (G : Space d → Space d) : Prop :=
…
```
Mentions: OAI.Bernoulli.Space
def OAI.Bernoulli.H1Loc line 43
Source documentation
Ballwise H¹_loc, on an open set (balls have compact closure inside D).
Also declared: ComparatorChallenges/BernoulliNonflatInSeven.lean:42 (same declaration text).
```
def H1Loc {d : ℕ} (D : Set (Space d))
    (u : Space d → ℝ) (G : Space d → Space d) : Prop :=
…
```
Mentions: OAI.Bernoulli.Space
def OAI.Bernoulli.energy line 49
Source documentation
The exact volume-one Bernoulli energy, not just Dirichlet energy.
Also declared: ComparatorChallenges/BernoulliNonflatInSeven.lean:48 (same declaration text).
```
def energy {d : ℕ} (D : Set (Space d))
    (u : Space d → ℝ) (G : Space d → Space d) : ℝ :=
…
```
Mentions: OAI.Bernoulli.Space
def OAI.Bernoulli.LocalMinimizer line 55
Source documentation
Full ballwise local comparison. Competitor and gradient are arbitrary Sobolev representatives on the ball, with zero-trace difference.
Also declared: ComparatorChallenges/BernoulliNonflatInSeven.lean:54 (same declaration text).
```
def LocalMinimizer {d : ℕ} (D : Set (Space d)) (u : Space d → ℝ) : Prop :=
…
```
Mentions: OAI.Bernoulli.Space
def OAI.Bernoulli.GlobalMinimizer line 66
Source documentation
Nonnegative global minimizer, with all centers and all positive radii.
Also declared: ComparatorChallenges/BernoulliNonflatInSeven.lean:65 (same declaration text).
```
def GlobalMinimizer {d : ℕ} (u : Space d → ℝ) : Prop :=
…
```
Mentions: OAI.Bernoulli.Space
def OAI.Bernoulli.OneHomogeneous line 69
Also declared: ComparatorChallenges/BernoulliNonflatInSeven.lean:68 (same declaration text).
def OAI.Bernoulli.Nonzero line 72
Also declared: ComparatorChallenges/BernoulliNonflatInSeven.lean:71 (same declaration text).
def OAI.Bernoulli.Flat line 76
Source documentation
Flatness is a.e. equality of H¹ representatives.
Also declared: ComparatorChallenges/BernoulliNonflatInSeven.lean:75 (same declaration text).
```
def Flat {d : ℕ} (u : Space d → ℝ) : Prop :=
…
```
Mentions: OAI.Bernoulli.Space