LargeChord.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Excluding large aligned-chord ratios

The secant estimate holds for every support. Reusing a support in the equality case makes the sign strict, and the literal inverse configuration gives the opposite image sign. A small radial perturbation then violates the actual defect bound. No compactness assumption on either ambient space is used here.

theorem OAI.Tingley.AlignedConfiguration.largeB_product_bounds line 28
Source documentation
The large-ratio secant bound controls both the product and the size of the support perturbation. All quantities come from the given configuration.
```
theorem largeB_product_bounds (hM : 0 < M) (ht : 0 < t ∧ t < 1)
    (hb : HasDefectBound f M) (hlarge : 1 - t < C.B) :
    1 - t ≤ C.A * C.u ∧ C.secantTheta ≤ 1 - C.B := by
…
```
Mentions: OAI.Tingley.HasDefectBound
theorem OAI.Tingley.AlignedConfiguration.largeB_forces_largeA_and_negative_support line 49
Source documentation
A large B makes every support at the original chord direction strictly negative on the base vector, and forces A into the same large regime.
```
theorem largeB_forces_largeA_and_negative_support
    (hM : 0 < M) (ht : 0 < t ∧ t < 1) (hb : HasDefectBound f M)
    (hlarge : 1 - t < C.B) :
    1 - t < C.A ∧
      ∀ L : X →L[ℝ] ℝ, SupportAt L (C.v : X) → L (y : X) < 0 := by
…
```
Mentions: OAI.Tingley.HasDefectBound, OAI.Tingley.SupportAt
theorem OAI.Tingley.AlignedConfiguration.largeB_support_signs line 112
Source documentation
The inverse uses literal negated directions. In particular, obtaining the positive image sign does not assume that the sphere map preserves antipodes.
```
theorem largeB_support_signs (hM : 0 < M) (ht : 0 < t ∧ t < 1)
    (hb : HasDefectBound f M) (hlarge : 1 - t < C.B) :
    (∀ L : X →L[ℝ] ℝ, SupportAt L (C.v : X) → L (y : X) < 0) ∧
      (∀ K : Y →L[ℝ] ℝ, SupportAt K (C.w : Y) → 0 < K (f y : Y)) := by
…
```
Mentions: OAI.Tingley.HasDefectBound, OAI.Tingley.SupportAt
theorem OAI.Tingley.AlignedConfiguration.largeB_impossible line 133
Source documentation
A small decrease of the radius strictly increases both contributions to the signed defect, contradicting its global bound.
```
theorem largeB_impossible (hM : 0 < M) (ht : 0 < t ∧ t < 1)
    (hb : HasDefectBound f M) (hlarge : 1 - t < C.B) : False := by
…
```
Mentions: OAI.Tingley.HasDefectBound
theorem OAI.Tingley.AlignedConfiguration.small_ratios line 164
Source documentation
Both ratios lie in the small regime. The first component is obtained by applying the already-proved contradiction to the exact inverse configuration.
```
theorem small_ratios (hM : 0 < M) (ht : 0 < t ∧ t < 1)
    (hb : HasDefectBound f M) : C.A ≤ 1 - t ∧ C.B ≤ 1 - t := by
…
```
Mentions: OAI.Tingley.HasDefectBound