OAI/Analysis/TreePotential/CostGeometry.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BoundedTreePotentials.FiniteMass line 15
2. instance OAI.BoundedTreePotentials.(instance at line 17) line 17
3. def OAI.BoundedTreePotentials.finiteMassPartial line 21
4. lemma OAI.BoundedTreePotentials.tendsto_finiteMassPartial line 30
5. lemma OAI.BoundedTreePotentials.iInf_finiteMass_eq line 34
6. theorem OAI.BoundedTreePotentials.linearCost_finite_mass line 52

   Source documentation

   The same linear infimum with exactly finite signed endpoint masses; no norm attainment or optimizer is inserted.

   theorem linearCost_finite_mass (B : L1Mass I →L[ℝ] H) (x : H) :
       linearCost B x = ⨅ μ : FiniteMass I, ‖x-B μ.val‖+‖μ.val‖ := by
   …

   Mentions: OAI.BoundedTreePotentials.L1Mass, OAI.BoundedTreePotentials.linearCost, OAI.BoundedTreePotentials.FiniteMass

7. theorem OAI.BoundedTreePotentials.quadraticCost_finite_mass line 60

   Source documentation

   Truncation also preserves the quadratic normalization, rather than replacing the Euclidean representation cost by a linear one.

   theorem quadraticCost_finite_mass (B : L1Mass I →L[ℝ] H) (x : H) :
       quadraticCost B x = ⨅ μ : FiniteMass I, Real.sqrt (‖x-B μ.val‖^2+‖μ.val‖^2) := by
   …

   Mentions: OAI.BoundedTreePotentials.L1Mass, OAI.BoundedTreePotentials.quadraticCost, OAI.BoundedTreePotentials.FiniteMass

8. lemma OAI.BoundedTreePotentials.sqrt_tail_shift line 68
9. lemma OAI.BoundedTreePotentials.CostHeads.linear_finite_center_compare line 79
10. theorem OAI.BoundedTreePotentials.CostHeads.linear_weak_sequence_clipping line 102

    Source documentation

    The center is approximated before taking the lower limit. Boundedness and weak nullity are retained, and the norm lower limit is the ordinary real liminf.

    theorem linear_weak_sequence_clipping (x : LinearOuter) (y : ℕ → LinearOuter)
        (hy : WeaklyNull y) (hbounded : BddAbove (Set.range (fun j => ‖y j‖))) :
        Real.sqrt (‖x‖^2+(Filter.liminf (fun j => ‖y j‖) atTop)^2/16) ≤
          Filter.liminf (fun j => max ‖x+y j‖ ‖x-y j‖) atTop := by
    …

    Mentions: OAI.BoundedTreePotentials.LinearOuter, OAI.BoundedTreePotentials.WeaklyNull

11. theorem OAI.BoundedTreePotentials.CostHeads.linear_bottom_up_outer line 141

    Source documentation

    Uniform bottom-up implication on the Hilbert sum; the changing finite heads are allowed to depend on j, and no fixed-head reduction is made.

    theorem linear_bottom_up_outer (A : ℕ → FiniteOuterHead) (x y : ℕ → LinearOuter)
        (hx : ∀ j, linearOuterHead (A j).nodes (A j).initial (x j) = x j)
        (hy : ∀ j, linearOuterHead (A j).nodes (A j).initial (y j) = 0)
        (hp : ∀ j, ‖x j+y j‖ ≤ 1) (hm : ∀ j, ‖x j-y j‖ ≤ 1)
        (hxn : Tendsto (fun j => ‖x j‖) atTop (𝓝 1)) :
        Tendsto (fun j => ‖y j‖) atTop (𝓝 0) := by
    …

    Mentions: OAI.BoundedTreePotentials.FiniteOuterHead, OAI.BoundedTreePotentials.LinearOuter, OAI.BoundedTreePotentials.CostHeads.linearOuterHead

12. theorem OAI.BoundedTreePotentials.CostHeads.quadratic_relative_tail_72 line 159

    Source documentation

    The finite head depends only on x,delta, not on the displacement.

    theorem quadratic_relative_tail_72 (x : QuadraticOuter) (hx : x ≠ 0)
        {δ : ℝ} (hδ : 0 < δ) (hδ1 : δ ≤ 1) :
        ∃ A : FiniteOuterHead, ∀ u : QuadraticOuter,
          ‖x+u‖ ≤ (1+δ)*‖x‖ → ‖x-u‖ ≤ (1+δ)*‖x‖ →
          ‖u-quadraticOuterHead A.nodes A.initial u‖ ≤ 72*Real.sqrt δ*‖x‖ := by
    …

    Mentions: OAI.BoundedTreePotentials.QuadraticOuter, OAI.BoundedTreePotentials.FiniteOuterHead, OAI.BoundedTreePotentials.CostHeads.quadraticOuterHead

13. lemma OAI.BoundedTreePotentials.CostHeads.quadratic_finite_center_compare line 200
14. lemma OAI.BoundedTreePotentials.lens_half_difference line 226
15. theorem OAI.BoundedTreePotentials.CostHeads.quadratic_lens_sixtyfour line 246

    Source documentation

    Infinite-lens obstruction using finite-rank heads and finite-center approximation. The denominator 64 implies the weaker numerical bounds.

    theorem quadratic_lens_sixtyfour (x : QuadraticOuter) (y : ℕ → QuadraticOuter)
        {R ε : ℝ} (hε : 0 < ε) (hp : ∀ j, ‖x+y j‖ ≤ R) (hm : ∀ j, ‖x-y j‖ ≤ R)
        (hsep : ∀ i j, i ≠ j → ε ≤ ‖y i-y j‖) :
        ‖x‖^2+ε^2/64 ≤ R^2 := by
    …

    Mentions: OAI.BoundedTreePotentials.QuadraticOuter

16. theorem OAI.BoundedTreePotentials.CostHeads.quadratic_lens_eight line 282
17. theorem OAI.BoundedTreePotentials.CostHeads.quadratic_lens_twelve line 289
18. theorem OAI.BoundedTreePotentials.CostHeads.quadratic_lens_seven line 296
19. theorem OAI.BoundedTreePotentials.CostHeads.quadratic_lens_nine line 306
20. def OAI.BoundedTreePotentials.maximumModulus line 325
21. lemma OAI.BoundedTreePotentials.averagedModulus_le_maximum line 330
22. lemma OAI.BoundedTreePotentials.fractional_energy_bound line 343
23. def OAI.BoundedTreePotentials.CostHeads.activeHead line 363

    Source documentation

    Empty heads are used exactly on zero components of the center.

    def activeHead (A : FiniteOuterHead) (x : QuadraticOuter) : FiniteOuterHead where
    …

    Mentions: OAI.BoundedTreePotentials.FiniteOuterHead, OAI.BoundedTreePotentials.QuadraticOuter

24. lemma OAI.BoundedTreePotentials.CostHeads.activeHead_center line 379
25. lemma OAI.BoundedTreePotentials.CostHeads.mem_active_tail line 389
26. theorem OAI.BoundedTreePotentials.CostHeads.quadratic_finite_centers line 406
27. theorem OAI.BoundedTreePotentials.CostHeads.quadratic_completed_centers line 424
28. theorem OAI.BoundedTreePotentials.CostHeads.quadratic_maximum_modulus line 443
29. theorem OAI.BoundedTreePotentials.CostHeads.quadratic_maximum_modulus_positive line 447
30. theorem OAI.BoundedTreePotentials.BlockCalculus.quadratic_component_estimate line 462