Polar.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ForestSpace.rawRestriction line 16
theorem OAI.ForestSpace.rawRestriction_apply line 19
theorem OAI.ForestSpace.norm_rawRestriction line 22
theorem OAI.ForestSpace.exists_raw_test line 38
Source documentation
Norming tests can always be chosen finitely supported, with a positive rather than absolute pairing.
```
 theorem exists_raw_test (x : FullDual V) {r : ℝ} (hr : r < ‖x‖) :
    ∃ u : TestVector V, ‖u‖ ≤ 1 ∧ r < x (u : J V) := by
…
```
Mentions: OAI.ForestSpace.FullDual, OAI.ForestSpace.TestVector, OAI.ForestSpace.J
def OAI.ForestSpace.Annihilates line 53
Source documentation
Vanishing on all finite tests in a specified coordinate region.
```
def Annihilates (x : FullDual V) (A : Set V) : Prop :=
…
```
Mentions: OAI.ForestSpace.FullDual
theorem OAI.ForestSpace.exists_head_test line 56
theorem OAI.ForestSpace.exists_tail_test line 66

theorem OAI.ForestSpace.paired_polar_test line 77

Source documentation

The cancellation of the same gate correction in the two dual evaluations.

 theorem paired_polar_test (H : Set V) {x y : FullDual V}
    (hx : Annihilates x Hᶜ) (hy : Annihilates y H)
    {f k c : TestVector V} (hf : SupportedOn f H) (hk : SupportedOn k Hᶜ)
    (hc : SupportedOn c Hᶜ) (s d : ℝ)
    (hp : ‖f + s • (c + k)‖ ≤ d) (hm : ‖f + s • (c - k)‖ ≤ d) :
    x (f : J V) + s * y (k : J V) ≤ (‖x+y‖ + ‖x-y‖) / 2 * d := by
…

Mentions: OAI.ForestSpace.FullDual, OAI.ForestSpace.Annihilates, OAI.ForestSpace.TestVector, OAI.ForestSpace.SupportedOn, OAI.ForestSpace.J

theorem OAI.ForestSpace.paired_parameter line 100
theorem OAI.ForestSpace.Annihilates.smul line 120
theorem OAI.ForestSpace.paired_estimate line 125
theorem OAI.ForestSpace.paired_two_parameters line 158
instance OAI.ForestSpace.fullDualAddCommGroup line 169
Distinct definitions of this name: ComparatorChallenges/ForestSpace.lean:341 (same statement text; different proof or body). Qualify references as OAI.ForestSpace.fullDualAddCommGroup@path.
def OAI.ForestSpace.e line 174
def OAI.ForestSpace.eStar line 177
Source documentation
The coordinate functional on J(T).
```
noncomputable def eStar (v : V) : FullDual V :=
…
```
Mentions: OAI.ForestSpace.FullDual
theorem OAI.ForestSpace.eStar_coe line 180
theorem OAI.ForestSpace.norm_e line 184
theorem OAI.ForestSpace.eStar_e line 187
theorem OAI.ForestSpace.eStar_norm_le line 190
theorem OAI.ForestSpace.norm_eStar line 197
def OAI.ForestSpace.coordinateSubspace line 204
Source documentation
The norm-closed coordinate span inside J(T)*. No identification with the full dual is made for a general forest.
```
@[reducible] noncomputable def coordinateSubspace (V : Type) [PartialOrder V] : Submodule ℝ (FullDual V) :=
…
```
Mentions: OAI.ForestSpace.FullDual
abbrev OAI.ForestSpace.X line 207