OAI/GroupTheory/Thompson/AnalyticScalarProfiles.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ThompsonNonamenability.Analytic.a line 15
2. def OAI.ThompsonNonamenability.Analytic.aDeriv line 19

   Source documentation

   The derivative profile of a, with its common values at the junctions.

   def aDeriv (t : ℝ) : ℝ :=
   …

3. def OAI.ThompsonNonamenability.Analytic.theta line 22
4. def OAI.ThompsonNonamenability.Analytic.thetaDeriv line 26

   Source documentation

   The derivative profile of theta.

   def thetaDeriv (t : ℝ) : ℝ :=
   …

5. def OAI.ThompsonNonamenability.Analytic.b line 30

   Source documentation

   The radial coefficient of the modified curve.

   def b (t : ℝ) : ℝ := min (a t) (-(1 / 8))

   Mentions: OAI.ThompsonNonamenability.Analytic.a

6. def OAI.ThompsonNonamenability.Analytic.q line 33

   Source documentation

   The bounded radial correction used in the tube.

   def q (t : ℝ) : ℝ := -max (a t + 1 / 8) 0

   Mentions: OAI.ThompsonNonamenability.Analytic.a

7. theorem OAI.ThompsonNonamenability.Analytic.a_of_le_two line 35
8. theorem OAI.ThompsonNonamenability.Analytic.a_of_two_lt_of_lt_three line 37
9. theorem OAI.ThompsonNonamenability.Analytic.a_of_three_le line 40
10. theorem OAI.ThompsonNonamenability.Analytic.aDeriv_of_le_two line 43
11. theorem OAI.ThompsonNonamenability.Analytic.aDeriv_of_three_le line 46
12. theorem OAI.ThompsonNonamenability.Analytic.theta_of_le_one line 49
13. theorem OAI.ThompsonNonamenability.Analytic.theta_of_one_lt_of_lt_two line 51
14. theorem OAI.ThompsonNonamenability.Analytic.theta_of_two_le line 54
15. theorem OAI.ThompsonNonamenability.Analytic.thetaDeriv_of_le_one line 57
16. theorem OAI.ThompsonNonamenability.Analytic.thetaDeriv_of_two_le line 60
17. theorem OAI.ThompsonNonamenability.Analytic.a_le_five_sixteenths line 63
18. theorem OAI.ThompsonNonamenability.Analytic.a_lower_of_one_le line 67
19. theorem OAI.ThompsonNonamenability.Analytic.a_lower_of_two_le line 75
20. theorem OAI.ThompsonNonamenability.Analytic.a_bounds_of_one_le line 83
21. theorem OAI.ThompsonNonamenability.Analytic.aDeriv_nonneg line 86
22. theorem OAI.ThompsonNonamenability.Analytic.aDeriv_le line 90
23. theorem OAI.ThompsonNonamenability.Analytic.thetaDeriv_nonneg line 94
24. theorem OAI.ThompsonNonamenability.Analytic.thetaDeriv_le line 98
25. theorem OAI.ThompsonNonamenability.Analytic.theta_nonneg line 102
26. theorem OAI.ThompsonNonamenability.Analytic.a_sub_bounds line 107

    Source documentation

    The ordered difference estimate also records monotonicity.

    theorem a_sub_bounds {x y : ℝ} (hxy : x ≤ y) :
        0 ≤ a y - a x ∧ a y - a x ≤ (y - x) / 8 := by
    …

    Mentions: OAI.ThompsonNonamenability.Analytic.a

27. theorem OAI.ThompsonNonamenability.Analytic.a_monotone line 135
28. theorem OAI.ThompsonNonamenability.Analytic.a_strictMonoOn line 140
29. theorem OAI.ThompsonNonamenability.Analytic.theta_sub_bounds line 146

    Source documentation

    Ordered differences of the angular profile.

    theorem theta_sub_bounds {x y : ℝ} (hxy : x ≤ y) :
        0 ≤ theta y - theta x ∧ theta y - theta x ≤ y - x := by
    …

    Mentions: OAI.ThompsonNonamenability.Analytic.theta

30. theorem OAI.ThompsonNonamenability.Analytic.theta_monotone line 174
31. theorem OAI.ThompsonNonamenability.Analytic.theta_strictMonoOn line 179
32. theorem OAI.ThompsonNonamenability.Analytic.lipschitz_of_ordered_sub line 203
33. theorem OAI.ThompsonNonamenability.Analytic.a_lipschitz line 214
34. theorem OAI.ThompsonNonamenability.Analytic.theta_lipschitz line 220
35. theorem OAI.ThompsonNonamenability.Analytic.aDeriv_eq_clip line 225
36. theorem OAI.ThompsonNonamenability.Analytic.thetaDeriv_eq_clip line 233
37. theorem OAI.ThompsonNonamenability.Analytic.aDeriv_lipschitz line 241
38. theorem OAI.ThompsonNonamenability.Analytic.thetaDeriv_lipschitz line 259
39. theorem OAI.ThompsonNonamenability.Analytic.q_eq_b_sub_a line 268
40. theorem OAI.ThompsonNonamenability.Analytic.q_nonpos line 276
41. theorem OAI.ThompsonNonamenability.Analytic.q_abs_le line 278
42. theorem OAI.ThompsonNonamenability.Analytic.q_eq_zero_of_a_le line 285
43. theorem OAI.ThompsonNonamenability.Analytic.q_eq_zero_of_le_neg_one line 288
44. theorem OAI.ThompsonNonamenability.Analytic.q_lipschitz line 293
45. theorem OAI.ThompsonNonamenability.Analytic.b_le line 303
46. theorem OAI.ThompsonNonamenability.Analytic.b_lipschitz line 305