TreeObstruction.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.IndependentProducts.child line 15
Source documentation
Natural enumeration of the positive-integer children.
```
def child (v : Vertex) (n : ℕ) : Vertex := v ++ [⟨n + 1, Nat.succ_pos n⟩]
…
```
Mentions: OAI.IndependentProducts.Vertex
def OAI.IndependentProducts.WeaklyNull line 22
Source documentation
Weak convergence to zero, stated directly against continuous real linear functionals.
```
def WeaklyNull (u : ℕ → X) : Prop :=
…
```
lemma OAI.IndependentProducts.weaklyNull_tendsto_finiteDimensional line 25
lemma OAI.IndependentProducts.weaklyNull_approx_cofinite line 36
Source documentation
A weakly null sequence approaches every closed finite-codimensional subspace in norm.
```
lemma weaklyNull_approx_cofinite {u : ℕ → X} (hu : WeaklyNull u)
    (F : Submodule ℝ X) (hF : F ∈ CofiniteSubspaces X) {ε : ℝ} (hε : 0 < ε) :
    ∀ᶠ n in atTop, ∃ z ∈ F, ‖u n - z‖ < ε := by
…
```
Mentions: OAI.IndependentProducts.WeaklyNull, OAI.IndependentProducts.CofiniteSubspaces

lemma OAI.IndependentProducts.oneSided_pos_subspace line 59

Source documentation

The elementary consequence of positivity of the actual inf-sup-inf modulus.

lemma oneSided_pos_subspace (N : Seminorm ℝ X) {t : ℝ}
    (hδ : 0 < oneSidedModulus X N t) {x : X} (hx : N x = 1) :
    ∃ F ∈ CofiniteSubspaces X, ∀ y ∈ F, N y = 1 →
      1 + oneSidedModulus X N t / 2 ≤ N (x + t • y) := by
…

Mentions: OAI.IndependentProducts.oneSidedModulus, OAI.IndependentProducts.CofiniteSubspaces

lemma OAI.IndependentProducts.seminorm_normalize line 98

lemma OAI.IndependentProducts.seminorm_radial_growth line 104

Source documentation

Convexity extends a positive one-sided gain from one radius to every larger radius.

lemma seminorm_radial_growth (N : Seminorm ℝ X) {x w : X} (hx : N x = 1)
    {t r γ : ℝ} (ht : 0 < t) (htr : t ≤ r) (hγ : 0 ≤ γ)
    (hg : 1 + γ ≤ N (x + t • w)) : 1 + γ ≤ N (x + r • w) := by
…

lemma OAI.IndependentProducts.seminorm_unit_subspace_growth line 120
lemma OAI.IndependentProducts.oneSided_pos_local_growth line 129
lemma OAI.IndependentProducts.not_finiteDimensional_of_weaklyNull_fixed_norm line 152
theorem OAI.IndependentProducts.bounded_tree_no_equivalent_auc line 164
Source documentation
The complete deterministic branch-growth obstruction. Its hypotheses concern the tree, not the existence or nonexistence of any renorming.
```
theorem bounded_tree_no_equivalent_auc (P : Vertex → X) (hP : ∀ v, ‖P v‖ = 1)
    {ρ : ℝ} (hρ : 0 < ρ)
    (hsize : ∀ v n, ‖P (child v n) - P v‖ = ρ)
    (hweak : ∀ v, WeaklyNull (fun n => P (child v n) - P v)) :
    ∀ N : Seminorm ℝ X, IsEquivalentNorm X N → ¬ IsAUC X N := by
…
```
Mentions: OAI.IndependentProducts.Vertex, OAI.IndependentProducts.child, OAI.IndependentProducts.WeaklyNull, OAI.IndependentProducts.IsEquivalentNorm, OAI.IndependentProducts.IsAUC