OAI/Analysis/SphereIsometry/ChordSecant.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Tingley.support_direction_lower line 22

   Source documentation

   The lower support bound uses the actual unit endpoint, and holds for every support at an earlier positive point of the same affine line.

   theorem support_direction_lower {v y : X} {p t θ : ℝ}
       (hy : ‖y‖ = 1) (hp : 0 < p) (ht : 0 < t)
       (hθ : 0 < θ) (hθβ : θ ≤ t / p)
       (hx : ‖p • v + t • y‖ = 1)
       (φ : X →L[ℝ] ℝ) (hφ : SupportAt φ (v + θ • y)) :
       (1 - t) / p ≤ φ v := by
   …

   Mentions: OAI.Tingley.SupportAt

2. def OAI.Tingley.AlignedConfiguration.secantStep line 67
3. def OAI.Tingley.AlignedConfiguration.secantTheta line 68
4. def OAI.Tingley.AlignedConfiguration.secantSlope line 69
5. theorem OAI.Tingley.AlignedConfiguration.secantStep_pos line 74
6. theorem OAI.Tingley.AlignedConfiguration.secantTheta_pos line 77
7. theorem OAI.Tingley.AlignedConfiguration.secantTheta_le line 80
8. theorem OAI.Tingley.AlignedConfiguration.secant_denominator_pos line 87
9. theorem OAI.Tingley.AlignedConfiguration.step_comparison_iff line 95
10. theorem OAI.Tingley.AlignedConfiguration.secantStep_eq_smallB line 103
11. theorem OAI.Tingley.AlignedConfiguration.secantStep_eq_largeB line 106
12. theorem OAI.Tingley.AlignedConfiguration.secant_radii_mem line 111
13. theorem OAI.Tingley.AlignedConfiguration.secant_defect_first line 125
14. theorem OAI.Tingley.AlignedConfiguration.secant_defect_opposite line 142
15. theorem OAI.Tingley.AlignedConfiguration.secant_weighted_identity line 159
16. theorem OAI.Tingley.AlignedConfiguration.secant_upper_smallB line 173
17. theorem OAI.Tingley.AlignedConfiguration.secant_upper_largeB line 196
18. theorem OAI.Tingley.AlignedConfiguration.secant_bounds line 221

    Source documentation

    No support is selected in this statement: it applies to every norm-bounded functional norming the displayed vector, including the support reused in the strictness argument.

    theorem secant_bounds (hM : 0 < M) (ht : 0 < t ∧ t < 1)
        (hb : HasDefectBound f M) (φ : X →L[ℝ] ℝ)
        (hφ : SupportAt φ ((C.v : X) + C.secantTheta • (y : X))) :
        (1 - t) / C.p ≤ φ C.v ∧ φ C.v ≤ C.secantSlope ∧
          (C.B ≤ 1 - t → C.secantSlope ≤ 1 - C.B) ∧
          (1 - t < C.B → C.secantSlope ≤ C.B) := by
    …

    Mentions: OAI.Tingley.HasDefectBound, OAI.Tingley.SupportAt

19. theorem OAI.Tingley.AlignedConfiguration.small_secant_product line 256