FiniteLaw.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.FiniteLaw.expect_comm line 38
theorem OAI.HyperbolicObstruction.FiniteLaw.expect_le_of_totalVariation line 48
theorem OAI.HyperbolicObstruction.FiniteLaw.totalVariation_comm line 55
theorem OAI.HyperbolicObstruction.ConeData.abs_pairing_le line 64
theorem OAI.HyperbolicObstruction.ConeData.normSq_inductiveMean_le line 82
theorem OAI.HyperbolicObstruction.ConeData.dist_inductiveMean_le line 101

theorem OAI.HyperbolicObstruction.ConeData.conditional_test line 111

Source documentation

The manuscript's quantitative conditional test. The hypotheses describe an actual finite coupling, with all of its branch and leaf errors explicit. The action-dependent function is not required to be independent of the law.

theorem conditional_test {α β ι : Type*} [Fintype α] [Fintype β]
    [Fintype ι] [Nonempty ι] (h : CATZero X)
    (μ : FiniteLaw α) (κ : FiniteLaw β) (v : ι → X)
    (hbar : ∀ u, (𝔼 i, T.pairing u (v i)) ≤ 0)
    (hen : (𝔼 i, T.normSq (v i)) = 1)
    (test : α → X) (letter : α → ι) (n : ℕ)
    (branch : Fin (n + 1) → β → α)
    (agree : ∀ j b, test (branch j b) = test (branch 0 b))
    {M B η : ℝ} (hM : 0 ≤ M) (hB : 0 ≤ B)
    (hv : ∀ i, dist T.vertex (v i) ≤ M)
    (htest : ∀ a, dist T.vertex (test a) ≤ B)
    (hbranch : ∀ j, (κ.map (branch j)).totalVariation μ ≤ η)
…

Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.FiniteLaw

theorem OAI.HyperbolicObstruction.conditional_test_eventually line 195

Source documentation

Passing to the limit in the quantitative conditional test, first with sample size fixed and then letting it tend to infinity.

theorem conditional_test_eventually {a : ℕ → ℝ} {B M : ℝ}
    (hbound : ∀ n : ℕ, ∃ η : ℕ → ℝ, Tendsto η atTop (𝓝 0) ∧
      ∀ᶠ ν in atTop, a ν ≤ B * Real.sqrt (1 / (n + 1 : ℝ) + 2 * M ^ 2 * η ν) +
        2 * B * M * η ν) :
    ∀ ε : ℝ, 0 < ε → ∀ᶠ ν in atTop, a ν < ε := by
…

theorem OAI.HyperbolicObstruction.FiniteLaw.expect_le_density line 219
theorem OAI.HyperbolicObstruction.FiniteLaw.expect_map_le_uniform line 227
theorem OAI.HyperbolicObstruction.GeometricAction.displacement_inv line 240
theorem OAI.HyperbolicObstruction.GeometricAction.displacement_mul_le line 249
theorem OAI.HyperbolicObstruction.GeometricAction.displacement_prod_le line 255

theorem OAI.HyperbolicObstruction.GeometricAction.six_letter_displacement_bound line 266

Source documentation

Averaging the actual six-letter relations gives the uniform displacement bound. Marginal domination is pointwise, so no independence of the action chosen after the rows is needed.

theorem six_letter_displacement_bound {α ι : Type*} [Fintype α] [Fintype ι]
    [Nonempty ι] (A : GeometricAction G X) (x : X) (letter : ι → G)
    (hen : (𝔼 i, dist x (A.act (letter i) x) ^ 2) = 1)
    (a : G) (κ : FiniteLaw α) (row : α → Fin 5 → ι)
    (hrow : ∀ b, (List.ofFn (letter ∘ row b)).prod = a⁻¹)
    {R : ℝ} (hmarg : ∀ j i, (κ.map (fun b => row b j)).mass i ≤ R / Fintype.card ι) :
    dist x (A.act a x) ^ 2 ≤ 25 * R := by
…

Mentions: OAI.HyperbolicObstruction.GeometricAction, OAI.HyperbolicObstruction.FiniteLaw

theorem OAI.HyperbolicObstruction.CATZero.quadrilateral_saturation line 304
Source documentation
The exact equality case of the quadrilateral inequality, also used for hexagons whose diagonals have squared length at least three.
```
theorem quadrilateral_saturation (h : CATZero X) (a b c d : X) (r s : ℝ)
    (hac : r ≤ dist a c ^ 2) (hbd : s ≤ dist b d ^ 2)
    (hsides : dist a b ^ 2 + dist b c ^ 2 + dist c d ^ 2 + dist d a ^ 2 = r + s) :
    dist a c ^ 2 = r ∧ dist b d ^ 2 = s ∧ mid h a c = mid h b d := by
…
```
Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.CATZero.mid
structure OAI.HyperbolicObstruction.MetricHexagon line 319
Source documentation
Six cyclic vertices, with exactly the path information obtained from the square decorations and admissible three-edge paths.
```
structure MetricHexagon {X : Type*} [MetricSpace X] (z : Fin 6 → X) : Prop where
…
```
def OAI.HyperbolicObstruction.hexDistSq line 325
Source documentation
The squared distances, by cyclic separation, not planar hexagon angles.
```
def hexDistSq (i j : Fin 6) : ℕ :=
…
```
lemma OAI.HyperbolicObstruction.hexDistSq_opposite_sum line 329
lemma OAI.HyperbolicObstruction.hexDistSq_opposite line 333
theorem OAI.HyperbolicObstruction.MetricHexagon.rigidity line 339
theorem OAI.HyperbolicObstruction.MetricHexagon.radius line 464
Source documentation
The radius squared at the common opposite-pair midpoint.
```
theorem radius (D : MetricHexagon z) (h : CATZero X) (j : Fin 6) :
    dist (CATZero.mid h (z 0) (z 3)) (z j) ^ 2 = 3 / 4 := by
…
```
Mentions: OAI.HyperbolicObstruction.MetricHexagon, OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.CATZero.mid