OAI/Analysis/DiamondDistortion/MidpointHeads.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.DiamondDistortion.Midpoint.Heads line 21

   Source documentation

   An actual family of allowed finite-rank coordinate heads. Approximation is by a vector fixed by a head; no uniform bound on projection norms is imposed.

   structure Heads (ι : Type*) (X : Type*) [NormedAddCommGroup X] [NormedSpace ℝ X] where
   …

2. lemma OAI.DiamondDistortion.Midpoint.finite_dimensional_pair line 30

   Source documentation

   Image compactness, with a finite-dimensional target and no assumption that a supremum over a sequence is attained.

   lemma finite_dimensional_pair [FiniteDimensional ℝ Y] (P : X →L[ℝ] Y)
       (z : ℕ → X) {R η : ℝ} (hz : ∀ i,‖z i‖ ≤ R) (hη : 0 < η) :
       ∃ i j : ℕ,i ≠ j ∧ ‖P ((1/2:ℝ) • (z i-z j))‖ < η := by
   …

3. lemma OAI.DiamondDistortion.Midpoint.finite_rank_pair line 45
4. lemma OAI.DiamondDistortion.Midpoint.average_lens line 53
5. lemma OAI.DiamondDistortion.Midpoint.pair_errors line 68
6. lemma OAI.DiamondDistortion.Midpoint.quotient_pair line 106

   Source documentation

   The quotient version chooses an actual nearby subspace vector, not just a formal quotient with small norm. Closedness and true finite codimension are explicit.

   lemma quotient_pair (F : Submodule ℝ X) [IsClosed (F : Set X)]
       [FiniteDimensional ℝ (X ⧸ F)] (z : ℕ → X) {R η : ℝ}
       (hz : ∀ i,‖z i‖ ≤ R) (hη : 0 < η) :
       ∃ (i j : ℕ) (v : X),i ≠ j ∧ v ∈ F ∧ ‖(1/2:ℝ) • (z i-z j)-v‖ < η := by
   …

7. lemma OAI.DiamondDistortion.Midpoint.positive_limit_le line 127
8. lemma OAI.DiamondDistortion.Midpoint.Heads.pure_pair line 134
9. def OAI.DiamondDistortion.Midpoint.Heads.SquareInput line 146
10. def OAI.DiamondDistortion.Midpoint.Heads.RadialInput line 150
11. theorem OAI.DiamondDistortion.Midpoint.Heads.square_lens line 154
12. theorem OAI.DiamondDistortion.Midpoint.Heads.radial_lens line 172
13. def OAI.DiamondDistortion.Midpoint.Heads.ParametricInput line 189
14. theorem OAI.DiamondDistortion.Midpoint.Heads.parametric_lens line 193
15. def OAI.DiamondDistortion.Midpoint.QuotientGain line 214
16. lemma OAI.DiamondDistortion.Midpoint.quotient_parent_full_gain line 219
17. lemma OAI.DiamondDistortion.Midpoint.quotient_actual_child line 280

    Source documentation

    Approximate actual-child selection: the supremal full gain implies a strictly larger actual child at the half-gain threshold, never a maximum.

    lemma quotient_actual_child {t g D : ℝ} (ht : 0 < t) (hg : 0 < g)
        (hD : 1 ≤ D) (htD : t ≤ 1/(2*D)) (hX : QuotientGain X t g)
        {x : X} (z : ℕ → X) (hx : 1 ≤ ‖x‖) (hxD : ‖x‖ ≤ D)
        (hs : ∀ i j,i ≠ j → 2 ≤ ‖z i-z j‖) :
        ∃ i,‖x‖*(1+g/2) < max ‖x+z i‖ ‖x-z i‖ := by
    …

    Mentions: OAI.DiamondDistortion.Midpoint.QuotientGain