AnalyticRotation.lean`

30 declarations, 0 contain sorry, 0 declared as axioms

The rank-two rotations in the displacement construction

These are actual bounded operators on a real inner-product space. The formula has no choice of orthogonal complement and remains valid when the two unit vectors coincide. The estimates use the operator norm.

def OAI.ThompsonNonamenability.Analytic.skew line 31
Source documentation
The skew rank-two operator associated with an ordered pair.
```
def skew (u v : E) : E →L[ℝ] E :=
…
```
Mentions: OAI.ThompsonNonamenability.Analytic.u, OAI.ThompsonNonamenability.Analytic.v
theorem OAI.ThompsonNonamenability.Analytic.skew_apply line 34
def OAI.ThompsonNonamenability.Analytic.rotation line 38
Source documentation
The rotation taking u to v, on the non-antipodal unit-pair domain.
```
def rotation (u v : E) : E →L[ℝ] E :=
…
```
Mentions: OAI.ThompsonNonamenability.Analytic.u, OAI.ThompsonNonamenability.Analytic.v
theorem OAI.ThompsonNonamenability.Analytic.rotation_apply line 42
theorem OAI.ThompsonNonamenability.Analytic.skew_self line 46
theorem OAI.ThompsonNonamenability.Analytic.rotation_self line 49
theorem OAI.ThompsonNonamenability.Analytic.skew_inner line 53
theorem OAI.ThompsonNonamenability.Analytic.rotation_apply_explicit line 60
theorem OAI.ThompsonNonamenability.Analytic.rotation_apply_self line 75
theorem OAI.ThompsonNonamenability.Analytic.rotation_inner line 84
theorem OAI.ThompsonNonamenability.Analytic.rotation_norm line 101
theorem OAI.ThompsonNonamenability.Analytic.norm_rotation_le_one line 107
theorem OAI.ThompsonNonamenability.Analytic.norm_rotation line 114
theorem OAI.ThompsonNonamenability.Analytic.rotation_inner_swap line 122
theorem OAI.ThompsonNonamenability.Analytic.rotation_reverse_apply line 131
theorem OAI.ThompsonNonamenability.Analytic.rotation_surjective line 138
def OAI.ThompsonNonamenability.Analytic.rankOne line 146
def OAI.ThompsonNonamenability.Analytic.rotationPolynomial line 149
Source documentation
The operator polynomial used in the rank-two rotation formula.
```
def rotationPolynomial (A : E →L[ℝ] E) (c : ℝ) : E →L[ℝ] E :=
…
```
lemma OAI.ThompsonNonamenability.Analytic.norm_rankOne line 152
lemma OAI.ThompsonNonamenability.Analytic.rankOne_sub line 155
lemma OAI.ThompsonNonamenability.Analytic.norm_rankOne_sub_le line 164
lemma OAI.ThompsonNonamenability.Analytic.norm_skew_le_two line 171
lemma OAI.ThompsonNonamenability.Analytic.norm_skew_sub_le line 177
lemma OAI.ThompsonNonamenability.Analytic.inner_sub_inner_le line 196
lemma OAI.ThompsonNonamenability.Analytic.inverse_one_add_bounds line 211
lemma OAI.ThompsonNonamenability.Analytic.inverse_one_add_difference line 217

lemma OAI.ThompsonNonamenability.Analytic.norm_rotationPolynomial_sub_le line 233

Source comment

This lemma is independent of the rank-two construction.

lemma norm_rotationPolynomial_sub_le (A B : E →L[ℝ] E) (c c' d : ℝ)
    (hd : 0 ≤ d) (hA : ‖A‖ ≤ 2) (hB : ‖B‖ ≤ 2)
    (hAB : ‖A - B‖ ≤ 2 * d) (hcc' : |c - c'| ≤ d)
    (hc' : |c'| ≤ 1) :
    ‖rotationPolynomial A c - rotationPolynomial B c'‖ ≤ 14 * d := by
…

Mentions: OAI.ThompsonNonamenability.Analytic.rotationPolynomial

lemma OAI.ThompsonNonamenability.Analytic.norm_rotation_sub_le line 285

theorem OAI.ThompsonNonamenability.Analytic.rotation_lipschitzWith line 300

Source documentation

Lipschitz dependence of the actual operators on two unit-vector families.

theorem rotation_lipschitzWith {X : Type uX} [PseudoMetricSpace X]
    (u v : X → E) {Ku Kv : ℝ≥0}
    (hu : ∀ x, ‖u x‖ = 1) (hv : ∀ x, ‖v x‖ = 1)
    (hκ : ∀ x, 0 ≤ ⟪u x, v x⟫_ℝ)
    (hLu : LipschitzWith Ku u) (hLv : LipschitzWith Kv v) :
    LipschitzWith (14 * (Ku + Kv)) (fun x => rotation (u x) (v x)) := by
…

Mentions: OAI.ThompsonNonamenability.Analytic.u, OAI.ThompsonNonamenability.Analytic.v, OAI.ThompsonNonamenability.Analytic.rotation

theorem OAI.ThompsonNonamenability.Analytic.rotation_lipschitzWith_238 line 323