OAI/Analysis/TreePotential/WeakNull.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoundedTreePotentials.WeaklyNull line 16

   Source documentation

   Weak convergence to zero, expressed by all continuous real linear tests.

   def WeaklyNull (d : ℕ → E) : Prop :=
   …

2. lemma OAI.BoundedTreePotentials.WeaklyNull.map line 19
3. def OAI.BoundedTreePotentials.functionalKernel line 23
4. lemma OAI.BoundedTreePotentials.WeaklyNull.approximable line 30

   Source documentation

   Weak nullity really gives approximation in every closed finite-codimensional subspace; the finite-dimensional quotient step is proved explicitly.

   lemma WeaklyNull.approximable {d : ℕ → E} (hd : WeaklyNull d) (F : ClosedFiniteCodim E)
       {ε : ℝ} (hε : 0 < ε) :
       ∀ᶠ n in atTop, ∃ w : E, w ∈ F.space ∧ ‖d n - w‖ < ε := by
   …

   Mentions: OAI.BoundedTreePotentials.WeaklyNull, OAI.BoundedTreePotentials.ClosedFiniteCodim

5. lemma OAI.BoundedTreePotentials.hilbert_upper_eval_sq_sum line 53
6. lemma OAI.BoundedTreePotentials.weaklyNull_of_hilbert_upper line 74
7. lemma OAI.BoundedTreePotentials.oneSidedModulus_nonneg line 84
8. lemma OAI.BoundedTreePotentials.oneSided_sphere_tail line 97
9. lemma OAI.BoundedTreePotentials.norm_bound_extends_to_rays line 114
10. lemma OAI.BoundedTreePotentials.oneSided_wide_tail line 139
11. lemma OAI.BoundedTreePotentials.oneSided_growth line 166

    Source documentation

    One weakly-null child sequence gives a definite AUC increase.

    lemma oneSided_growth {t γ c : ℝ} (ht : 0 < t) (hγ : 0 < γ) (hc : 0 < c)
        (hδ : (γ : EReal) < oneSidedModulus E t) (p : E) (hp : 0 < ‖p‖)
        (htp : t * ‖p‖ ≤ c/2) (d : ℕ → E) (hd : WeaklyNull d)
        (hdn : ∀ n, c ≤ ‖d n‖) :
        ∃ n, ‖p‖ + γ * ‖p‖ / 2 ≤ ‖p + d n‖ := by
    …

    Mentions: OAI.BoundedTreePotentials.oneSidedModulus, OAI.BoundedTreePotentials.WeaklyNull

12. def OAI.BoundedTreePotentials.child line 191
13. lemma OAI.BoundedTreePotentials.child_length line 194
14. lemma OAI.BoundedTreePotentials.exists_pos_real_lt_ereal line 197
15. theorem OAI.BoundedTreePotentials.bounded_tree_modulus_eq_zero line 209

    Source documentation

    The bounded-tree obstruction for arbitrary finite heights. Weak nullity is tested against the whole dual; iteration of the positive per-step gain gives the contradiction.

    theorem bounded_tree_modulus_eq_zero
        (p : (h : ℕ) → Tree h → E) {m M c : ℝ}
        (hm : 0 < m) (hmM : m ≤ M) (hc : 0 < c)
        (hbound : ∀ h, 1 ≤ h → ∀ s : Tree h, m ≤ ‖p h s‖ ∧ ‖p h s‖ ≤ M)
        (hweak : ∀ h, 1 ≤ h → ∀ (s : Tree h) (hs : s.val.length < h),
          WeaklyNull (fun n => p h (child s hs n) - p h s))
        (hinc : ∀ h, 1 ≤ h → ∀ (s : Tree h) (hs : s.val.length < h) (n : ℕ),
          c ≤ ‖p h (child s hs n) - p h s‖) :
        oneSidedModulus E (c / (2 * M)) = 0 := by
    …

    Mentions: OAI.BoundedTreePotentials.Tree, OAI.BoundedTreePotentials.WeaklyNull, OAI.BoundedTreePotentials.child, OAI.BoundedTreePotentials.oneSidedModulus

16. theorem OAI.BoundedTreePotentials.bounded_tree_renorming_obstruction line 265

    Source documentation

    Explicit equivalence constants are retained in the obstruction radius. Quantification over continuous linear copies is precisely quantification over equivalent norms via the identity linear equivalence.

    theorem bounded_tree_renorming_obstruction
        {Y : Type*} [NormedAddCommGroup Y] [NormedSpace ℝ Y]
        (p : (h : ℕ) → Tree h → E) {m M c α β : ℝ}
        (hm : 0 < m) (hmM : m ≤ M) (hc : 0 < c)
        (hbound : ∀ h, 1 ≤ h → ∀ s : Tree h, m ≤ ‖p h s‖ ∧ ‖p h s‖ ≤ M)
        (hweak : ∀ h, 1 ≤ h → ∀ (s : Tree h) (hs : s.val.length < h),
          WeaklyNull (fun n => p h (child s hs n) - p h s))
        (hinc : ∀ h, 1 ≤ h → ∀ (s : Tree h) (hs : s.val.length < h) (n : ℕ),
          c ≤ ‖p h (child s hs n) - p h s‖)
        (e : E ≃L[ℝ] Y) (hα : 0 < α) (hαβ : α ≤ β)
        (he : ∀ x : E, α * ‖x‖ ≤ ‖e x‖ ∧ ‖e x‖ ≤ β * ‖x‖) :
        oneSidedModulus Y (α * c / (2 * β * M)) = 0 := by
    …

    Mentions: OAI.BoundedTreePotentials.Tree, OAI.BoundedTreePotentials.WeaklyNull, OAI.BoundedTreePotentials.child, OAI.BoundedTreePotentials.oneSidedModulus