OAI/Geometry/HyperbolicGroups/ConditionalStar.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.ConditionalStar line 53

   Source documentation

   A conditional star: branches agree exactly on the named fields. The finite law placed on it below need not be uniform.

   def ConditionalStar {F L Ω : Type*} [DecidableEq F] (label : Ω → F → L)
       (I : Finset F) (k : ℕ) :=
   …

2. instance OAI.HyperbolicObstruction.ConditionalStar.(instance at line 59) line 59
3. def OAI.HyperbolicObstruction.ConditionalStar.branch line 63
4. lemma OAI.HyperbolicObstruction.ConditionalStar.agree line 65
5. structure OAI.HyperbolicObstruction.SamplingSequence line 73

   Source documentation

   Only combinatorial sampling assertions occur here, independent of the action that may be chosen after the random tables have been exposed. This is not a replacement for the random-table producer.

   structure SamplingSequence (F : Type*) [DecidableEq F] (Admissible : Finset F → Prop)
       (L Ω : ℕ → Type*) [∀ n, Fintype (L n)] [∀ n, Nonempty (L n)]
       [∀ n, DecidableEq (L n)] [∀ n, Fintype (Ω n)] [∀ n, Nonempty (Ω n)]
       (label : ∀ n, Ω n → F → L n) where
   …

6. structure OAI.HyperbolicObstruction.EnergyOrbit line 88

   Source documentation

   Actual normalized orbit points along a symmetric finite generator list.

   structure EnergyOrbit (L X : Type*) [Fintype L] [MetricSpace X] (M : ℝ) where
   …

7. abbrev OAI.HyperbolicObstruction.EnergyOrbit.Cone line 101
8. abbrev OAI.HyperbolicObstruction.EnergyOrbit.cone line 102
9. def OAI.HyperbolicObstruction.EnergyOrbit.vector line 104
10. lemma OAI.HyperbolicObstruction.EnergyOrbit.normSq_vector line 106
11. lemma OAI.HyperbolicObstruction.EnergyOrbit.norm_vector line 109
12. lemma OAI.HyperbolicObstruction.EnergyOrbit.barycenter line 113
13. lemma OAI.HyperbolicObstruction.EnergyOrbit.energy_vector line 119
14. lemma OAI.HyperbolicObstruction.EnergyOrbit.barycenter_read line 123
15. lemma OAI.HyperbolicObstruction.EnergyOrbit.energy_read line 128
16. theorem OAI.HyperbolicObstruction.SamplingSequence.conditional line 147

    Source documentation

    The conditional test applies to arbitrary bounded action-dependent tests, including tests using inverses of any field labels.

    theorem conditional {I : Finset F} {e : F} (he : e ∉ I) (hI : Admissible (insert e I))
        (σ : ∀ n, L n ≃ L n) (test : ∀ n, Ω n → (O n).Cone)
        (depends : ∀ n a b, (∀ i ∈ I, label n a i = label n b i) → test n a = test n b)
        {B : ℝ} (hM : 0 ≤ M) (hB : 0 ≤ B)
        (htest : ∀ n a, dist (O n).cone.vertex (test n a) ≤ B) :
        ∀ ε : ℝ, 0 < ε → ∀ᶠ n in atTop,
          (𝔼 a, (O n).cone.pairing (test n a) ((O n).vector (σ n (label n a e)))) < ε := by
    …

17. theorem OAI.HyperbolicObstruction.SamplingSequence.edge_energy line 171

    Source documentation

    Single-field convergence remains usable uniformly after the action has been chosen: the displacement functions only need the uniform letter bound.

    theorem edge_energy (e : F) (σ : ∀ n, L n ≃ L n) (hM : 0 ≤ M) :
        Tendsto (fun n => 𝔼 a, dist (O n).base ((O n).isom (σ n (label n a e)) (O n).base) ^ 2)
          atTop (𝓝 1) := by
    …

18. theorem OAI.HyperbolicObstruction.EnergyOrbit.exists_of_geometric line 213

    Source documentation

    Six-letter relative counts provide the bound M=8 for the rescaled genuine geometric action; no bound on the action is assumed before sampling.

    theorem exists_of_geometric {L G X : Type*} [Fintype L] [Nonempty L] [Group G]
        [Infinite G] [MetricSpace X] [Nonempty X] [ProperSpace X]
        (hX : CATZero X) (A : GeometricAction G X) (letter : L → G) (inv : L ≃ L)
        (hinv : ∀ i, letter (inv i) = (letter i)⁻¹)
        (hgen : Subgroup.closure (Set.range letter) = ⊤)
        (Row : L → Type*) [∀ i, Fintype (Row i)] (κ : ∀ i, FiniteLaw (Row i))
        (row : ∀ i, Row i → Fin 5 → L)
        (hrow : ∀ i b, (List.ofFn (letter ∘ row i b)).prod = (letter i)⁻¹)
        (hmarg : ∀ i j a, ((κ i).map (fun b => row i b j)).mass a ≤ 2 / Fintype.card L) :
        ∃ r : ℝ, ∃ hr : 0 < r, ∃ O : EnergyOrbit L (MetricScale.Space r hr X) 8,
          ∀ i, O.isom i = MetricScale.action A.act (letter i) := by
    …

    Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.GeometricAction, OAI.HyperbolicObstruction.FiniteLaw, OAI.HyperbolicObstruction.EnergyOrbit, OAI.HyperbolicObstruction.MetricScale.Space, OAI.HyperbolicObstruction.MetricScale.action

19. lemma OAI.HyperbolicObstruction.IsometricAction.displacement_mul_dist line 240
20. def OAI.HyperbolicObstruction.OrbitWord.word line 254
21. lemma OAI.HyperbolicObstruction.OrbitWord.nil line 257
22. lemma OAI.HyperbolicObstruction.OrbitWord.cons line 260
23. lemma OAI.HyperbolicObstruction.OrbitWord.depends line 263
24. lemma OAI.HyperbolicObstruction.OrbitWord.bound line 271
25. theorem OAI.HyperbolicObstruction.SamplingSequence.word_lower line 300

    Source documentation

    Path lower bounds are produced from the sampling assertions and the action, not postulated as a limiting configuration. The proof uses only finite sums and one-sided vanishing errors, so the spaces/actions can vary with n.

    theorem word_lower (down : ∀ I J, I ⊆ J → Admissible J → Admissible I)
        (σ : ∀ n, F → L n ≃ L n) (hM : 0 ≤ M) (w : List F) (hw : w.Nodup)
        (hadm : Admissible w.toFinset) :
        ∀ ε : ℝ, 0 < ε → ∀ᶠ n in atTop,
          (w.length : ℝ) - ε ≤
            𝔼 a, dist (O n).base (A n (OrbitWord.word (label n) (σ n) (letter n) a w) (O n).base) ^ 2 := by
    …

    Mentions: OAI.HyperbolicObstruction.OrbitWord.word

26. lemma OAI.HyperbolicObstruction.CATZero.isometry_segment line 372
27. lemma OAI.HyperbolicObstruction.CATZero.fractional_log_comparison line 379

    Source documentation

    Comparison at fixed fractions is taken before forming the ultralimit.

    lemma fractional_log_comparison (h : CATZero X) (o x y : X) {a b : ℝ}
        (ha : a ∈ Set.Icc (0 : ℝ) 1) (hb : b ∈ Set.Icc (0 : ℝ) 1) :
        a ^ 2 * dist o x ^ 2 + b ^ 2 * dist o y ^ 2 -
          2 * a * b * (TangentCone.coneData h o).pairing
            (TangentCone.log h o x) (TangentCone.log h o y) ≤
          dist (segment h o x a) (segment h o y b) ^ 2 := by
    …

    Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.TangentCone.coneData, OAI.HyperbolicObstruction.TangentCone.log, OAI.HyperbolicObstruction.CATZero.segment

28. theorem OAI.HyperbolicObstruction.SamplingSequence.fractional_error line 409

    Source documentation

    Uniform fractional-distance comparison for any bounded point function of I, after translations depending on the whole match.

    theorem fractional_error {I : Finset F} {e : F} (he : e ∉ I)
        (hI : Admissible (insert e I)) (σ : ∀ n, L n ≃ L n)
        (test : ∀ n, Ω n → X n)
        (depends : ∀ n a b, (∀ i ∈ I, label n a i = label n b i) → test n a = test n b)
        {B : ℝ} (hM : 0 ≤ M) (hB : 0 ≤ B) (htest : ∀ n a, dist (O n).base (test n a) ≤ B)
        (frame : ∀ n, Ω n → X n ≃ᵢ X n) {a b : ℝ}
        (ha : a ∈ Set.Icc (0 : ℝ) 1) (hb : b ∈ Set.Icc (0 : ℝ) 1) :
        ∀ ε : ℝ, 0 < ε → ∀ᶠ n in atTop,
          a ^ 2 * (𝔼 m, dist (frame n m (O n).base) (frame n m (test n m)) ^ 2) +
            b ^ 2 * (𝔼 m, dist (frame n m (O n).base)
              (frame n m ((O n).isom (σ n (label n m e)) (O n).base)) ^ 2) - ε ≤
          𝔼 m, dist
    …