BoundaryHeight.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Scalar and vector boundary height estimates

Haar-volume distortion on ray quotients yields additive trace bounds after taking logarithms. Finitely many spanning traces then bound the full height error. A linear coefficient compatible with a sublinear error is unique.

theorem OAI.PolycyclicRecognition.abs_log_sub_le_of_comparison line 18

Source documentation

Uniform multiplicative comparison of positive quantities bounds the difference of their logarithms.

theorem abs_log_sub_le_of_comparison {a b K : ℝ} (ha : 0 < a) (hb : 0 < b)
    (hK : 0 < K) (hab : a ≤ K * b) (hba : b ≤ K * a) :
    |Real.log a - Real.log b| ≤ Real.log K := by
…

theorem OAI.PolycyclicRecognition.abs_sub_le_log_of_exp_comparison line 31

Source documentation

Applying the logarithmic comparison to exponential Jacobians.

theorem abs_sub_le_log_of_exp_comparison {a b K : ℝ} (hK : 0 < K)
    (hab : Real.exp a ≤ K * Real.exp b) (hba : Real.exp b ≤ K * Real.exp a) :
    |a - b| ≤ Real.log K := by
…

theorem OAI.PolycyclicRecognition.separates_of_dual_span line 38

Source documentation

A family of real linear forms spanning the dual separates points.

theorem separates_of_dual_span {W I : Type*} [AddCommGroup W] [Module ℝ W]
    (α : I → Module.Dual ℝ W)
    (hspan : Submodule.span ℝ (Set.range α) = ⊤)
    (w : W) (hw : ∀ i, α i w = 0) : w = 0 := by
…

theorem OAI.PolycyclicRecognition.exists_bound_of_separating_forms line 55

Source documentation

Finitely many separating trace bounds control the vector norm by one constant depending only on those traces.

theorem exists_bound_of_separating_forms {W I : Type*}
    [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ W] [Fintype I]
    (α : I → Module.Dual ℝ W)
    (hsep : ∀ w, (∀ i, α i w = 0) → w = 0) :
    ∃ C : ℝ, 0 < C ∧ ∀ (w : W) (B : ℝ), 0 ≤ B →
      (∀ i, |α i w| ≤ B) → ‖w‖ ≤ C * B := by
…

theorem OAI.PolycyclicRecognition.exists_bound_of_dual_span line 79

Source documentation

In the boundary argument the ray traces span the dual height space.

theorem exists_bound_of_dual_span {W I : Type*}
    [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ W] [Fintype I]
    (α : I → Module.Dual ℝ W)
    (hspan : Submodule.span ℝ (Set.range α) = ⊤) :
    ∃ C : ℝ, 0 < C ∧ ∀ (w : W) (B : ℝ), 0 ≤ B →
      (∀ i, |α i w| ≤ B) → ‖w‖ ≤ C * B :=
…

theorem OAI.PolycyclicRecognition.eq_zero_of_sublinear_linear_bound line 89
Source documentation
Bounded error plus arbitrarily small linear error cannot hide a nonzero linear coefficient. This identifies each source trace with its target trace.
```
theorem eq_zero_of_sublinear_linear_bound {c B : ℝ}
    (h : ∀ ε : ℝ, 0 < ε → ∃ R : ℝ, ∀ t : ℝ, R ≤ t → 0 ≤ t →
      |t * c| ≤ B + ε * t) : c = 0 := by
…
```

theorem OAI.PolycyclicRecognition.trace_eq_of_bounded_and_sublinear line 106

Source documentation

A uniformly bounded trace error determines its linear coefficient once the vector error is sublinear along every height ray.

theorem trace_eq_of_bounded_and_sublinear
    {W : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
    [FiniteDimensional ℝ W]
    (α β : Module.Dual ℝ W) (A : W →ₗ[ℝ] W)
    (profile : W → ℝ → W) (B : ℝ)
    (hbound : ∀ w t, 0 ≤ t → |β (profile w t) - t * α w| ≤ B)
    (hsub : ∀ w ε, 0 < ε → ∃ R : ℝ, ∀ t, R ≤ t → 0 ≤ t →
      ‖profile w t - t • A w‖ ≤ ε * t) :
    α = β.comp A := by
…