HorizontalDerivativeLabel.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The two segment inequalities determine the horizontal derivative label

theorem OAI.PolycyclicRecognition.horizontal_derivative_eq_support_symmetry line 18

Source documentation

Once the actual line derivatives define a linear horizontal map, the two segment inequalities force it to be one finite support-symmetry label after projection to height. No derivative-level inequalities are assumed.

theorem horizontal_derivative_eq_support_symmetry
    {V W I B J : Type*} [AddCommGroup V] [Module ℝ V]
    [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ W]
    [Fintype I] [Fintype B] [Nonempty B] [Finite J]
    (D : SupportDatum W I B) (π M : V →ₗ[ℝ] W) (hπ : Function.Surjective π)
    (A : J → linearSupportSymmetryGroup D)
    (curve : V → ℝ → W) (hcurve : ∀ v, Continuous (curve v))
    (hderiv : ∀ v, HasDerivAt (curve v) (M v) 0)
    (T₀ : V → ℝ) (hT₀ : ∀ v, 0 < T₀ v)
    (hinc : ∀ v t, 0 < t → t < T₀ v →
      t⁻¹ • (curve v t - curve v 0) ∈ convexHull ℝ (range fun j => (A j).val (π v)))
    (hvolume : ∀ v t, 0 < t → t < T₀ v →
…

Mentions: OAI.PolycyclicRecognition.SupportDatum, OAI.PolycyclicRecognition.linearSupportSymmetryGroup

theorem OAI.PolycyclicRecognition.horizontal_derivative_eq_one_of_labels line 44

Source documentation

The derivative belongs to the original finite family of labels, rather than just its containing segment-norm isometry group.

theorem horizontal_derivative_eq_one_of_labels
    {V W I B J : Type*} [AddCommGroup V] [Module ℝ V]
    [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ W]
    [Fintype I] [Fintype B] [Nonempty B] [Finite J]
    (D : SupportDatum W I B) (π M : V →ₗ[ℝ] W) (hπ : Function.Surjective π)
    (A : J → linearSupportSymmetryGroup D)
    (curve : V → ℝ → W) (hcurve : ∀ v, Continuous (curve v))
    (hderiv : ∀ v, HasDerivAt (curve v) (M v) 0)
    (T₀ : V → ℝ) (hT₀ : ∀ v, 0 < T₀ v)
    (hinc : ∀ v t, 0 < t → t < T₀ v →
      t⁻¹ • (curve v t - curve v 0) ∈ convexHull ℝ (range fun j => (A j).val (π v)))
    (hvolume : ∀ v t, 0 < t → t < T₀ v →
…

Mentions: OAI.PolycyclicRecognition.SupportDatum, OAI.PolycyclicRecognition.linearSupportSymmetryGroup

theorem OAI.PolycyclicRecognition.horizontal_derivative_eq_one_of_template_labels line 69

Source documentation

Specialization to the manuscript's template-preserving labels.

theorem horizontal_derivative_eq_one_of_template_labels
    {V W I B J : Type*} [AddCommGroup V] [Module ℝ V]
    [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ W]
    [Fintype I] [Fintype B] [Nonempty B] [Finite J]
    (D : SupportDatum W I B) (π M : V →ₗ[ℝ] W) (hπ : Function.Surjective π)
    (A : J → templateSymmetryGroup D)
    (curve : V → ℝ → W) (hcurve : ∀ v, Continuous (curve v))
    (hderiv : ∀ v, HasDerivAt (curve v) (M v) 0)
    (T₀ : V → ℝ) (hT₀ : ∀ v, 0 < T₀ v)
    (hinc : ∀ v t, 0 < t → t < T₀ v →
      t⁻¹ • (curve v t - curve v 0) ∈ convexHull ℝ (range fun j => (A j).val (π v)))
    (hvolume : ∀ v t, 0 < t → t < T₀ v →
…

Mentions: OAI.PolycyclicRecognition.SupportDatum, OAI.PolycyclicRecognition.templateSymmetryGroup