CoordinatePredual.lean`

50 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SeparableQuotient.ActualSpace.norming line 12
Source documentation
The full norming set obtained from finite-stage pure and mixed operations.
```
def norming : NormingSet Γ where
…
```
abbrev OAI.SeparableQuotient.ActualSpace.E line 18
Source documentation
The actual real Banach space E of the CH construction.
```
abbrev E := norming.Space
```
instance OAI.SeparableQuotient.ActualSpace.EGroup line 20
instance OAI.SeparableQuotient.ActualSpace.ESpace line 21
instance OAI.SeparableQuotient.ActualSpace.ETopologicalAdd line 22
instance OAI.SeparableQuotient.ActualSpace.EContinuousAdd line 24
instance OAI.SeparableQuotient.ActualSpace.(instance at line 26) line 26
instance OAI.SeparableQuotient.ActualSpace.(instance at line 28) line 28
lemma OAI.SeparableQuotient.ActualSpace.infiniteDimensional line 31
abbrev OAI.SeparableQuotient.ActualSpace.e line 33
abbrev OAI.SeparableQuotient.ActualSpace.coordinate line 34
lemma OAI.SeparableQuotient.ActualSpace.norm_e line 36
lemma OAI.SeparableQuotient.ActualSpace.support_countable line 38
lemma OAI.SeparableQuotient.ActualSpace.coordinate_ext line 41
lemma OAI.SeparableQuotient.ActualSpace.cropStable line 44
def OAI.SeparableQuotient.ActualSpace.projection line 48
Source documentation
Every ordinal/color rectangle projection is defined on the full completion.
```
def projection (A : Crop) : E →L[ℝ] E := norming.projection (A.set .mixed) (cropStable A)
```
Mentions: OAI.SeparableQuotient.ActualSpace.E, OAI.SeparableQuotient.ActualSpace.cropStable
lemma OAI.SeparableQuotient.ActualSpace.norm_projection_le line 50
lemma OAI.SeparableQuotient.ActualSpace.coordinate_projection line 55

lemma OAI.SeparableQuotient.ActualSpace.norm_includeFinite_on_color line 66

Source documentation

The ℓs-coordinate estimate on finite vectors.

lemma norm_includeFinite_on_color (k : ℕ) (x : Γ →₀ ℝ)
    (hx : ∀ a ∈ x.support, Colors.color a = k) :
    ‖norming.includeFinite x‖ ≤ ‖realArray (Family.pure k).primalExponent x‖ := by
…

Mentions: OAI.SeparableQuotient.Colors.color

lemma OAI.SeparableQuotient.Norming.Family.L_pos line 93
lemma OAI.SeparableQuotient.Norming.pure_typeI_mem line 97
Source documentation
Every finite successive family of existing normers has its prescribed Type I average in the same actual family.
```
lemma pure_typeI_mem (k : ℕ) (e : TypeI (.pure k))
    (h : ∀ i, e.child i ∈ Pure k) : e.value ∈ Pure k := by
…
```
Mentions: OAI.SeparableQuotient.Norming.TypeI, OAI.SeparableQuotient.Norming.Pure
lemma OAI.SeparableQuotient.Norming.mixed_typeI_mem line 107
def OAI.SeparableQuotient.Norming.coordinateAverage line 118
Source documentation
A concrete signed coordinate Type I expression.
```
def coordinateAverage (k j n : ℕ) (hj : 1 ≤ j) (hn : 1 ≤ n)
    (hnj : n ≤ (Family.pure k).L j) (a : Fin n ↪o Γ)
    (c : Fin n → ℚ) (hc : ∀ i, c i ≠ 0) : TypeI (.pure k) where
…
```
Mentions: OAI.SeparableQuotient.Norming.Γ, OAI.SeparableQuotient.Norming.TypeI
lemma OAI.SeparableQuotient.Norming.coordinateAverage_mem line 135
abbrev OAI.SeparableQuotient.ActualSpace.X₀ line 153
abbrev OAI.SeparableQuotient.ActualSpace.coordinate₀ line 154
lemma OAI.SeparableQuotient.ActualSpace.signed_coordinate_bound line 163
lemma OAI.SeparableQuotient.ActualSpace.predual_large_coordinates_finite line 203
lemma OAI.SeparableQuotient.ActualSpace.predual_coordinate_support_countable line 236
Source documentation
Direct countable support of every candidate dual-predual vector, from the actual Type I operations and L_j/m_j→∞. No bounded completeness is assumed.
```
lemma predual_coordinate_support_countable (g : StrongDual ℝ X₀) :
    Set.Countable {a : Γ | g (coordinate₀ a) ≠ 0} := by
…
```
Mentions: OAI.SeparableQuotient.ActualSpace.X₀, OAI.SeparableQuotient.ActualSpace.coordinate₀
def OAI.SeparableQuotient.Norming.Crop.ordinalSet line 253
def OAI.SeparableQuotient.Norming.Crop.colorSet line 256
def OAI.SeparableQuotient.Norming.Crop.oneColor line 259
def OAI.SeparableQuotient.Norming.Crop.colorsBelow line 261
def OAI.SeparableQuotient.Norming.Crop.colorsFrom line 263
lemma OAI.SeparableQuotient.Norming.Crop.oneColor_set line 265
lemma OAI.SeparableQuotient.Norming.Crop.colorsBelow_set line 269
lemma OAI.SeparableQuotient.Norming.Crop.ordinalSet_set line 274
lemma OAI.SeparableQuotient.ActualSpace.evaluateArray_projection line 285
lemma OAI.SeparableQuotient.ActualSpace.evaluateArray_crop_of_zero line 290
lemma OAI.SeparableQuotient.ActualSpace.norm_le_of_pure line 296
Source documentation
The full and pure norms coincide on a single color.
```
lemma norm_le_of_pure (k : ℕ) (x : E) (hx : ∀ a, Colors.color a ≠ k → coordinate a x = 0)
    (r : ℝ) (hr : 0 ≤ r) (h : ∀ f ∈ Pure k, |norming.evaluateArray x f| ≤ r) : ‖x‖ ≤ r := by
…
```
Mentions: OAI.SeparableQuotient.ActualSpace.E, OAI.SeparableQuotient.Colors.color, OAI.SeparableQuotient.ActualSpace.coordinate
lemma OAI.SeparableQuotient.ActualSpace.exists_full_normer line 305
lemma OAI.SeparableQuotient.ActualSpace.exists_pure_normer line 318
lemma OAI.SeparableQuotient.ActualSpace.tendsto_colorsBelow line 333
def OAI.SeparableQuotient.Norming.Family.normers line 345
lemma OAI.SeparableQuotient.Norming.Family.normers_subset_full line 349
lemma OAI.SeparableQuotient.Norming.Family.typeI_mem line 354
lemma OAI.SeparableQuotient.Norming.Family.exists_large_ratio line 360
lemma OAI.SeparableQuotient.ActualSpace.predual_array_apply line 379
lemma OAI.SeparableQuotient.ActualSpace.predual_array_eq_evaluate line 384

lemma OAI.SeparableQuotient.ActualSpace.no_successive_positive_normers line 391

Source documentation

A Type I obstruction to successive uniformly positive normers.

lemma no_successive_positive_normers (g : StrongDual ℝ X₀) (t : Family)
    (f : ℕ → Array) (hf : ∀ i, f i ∈ t.normers)
    (hs : ∀ i j, i < j → Successive t (f i) (f j))
    (δ : ℝ) (hδ : 0 < δ) (hlarge : ∀ i, δ ≤ g (norming.rationalPredual (f i))) : False := by
…

Mentions: OAI.SeparableQuotient.ActualSpace.X₀