TemplateConeTraces.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Positive trace tests after a template symmetry

The pure-word multiplicities on a transformed cone give a positive test on each of its original extreme rays. The inverse template symmetry supplies actual generator weights on those rays.

theorem OAI.PolycyclicRecognition.positive_sum_on_weightCone_of_scaled_extremes line 20

theorem OAI.PolycyclicRecognition.templateSymmetry_weight_ray_surjective line 64

Source documentation

Every source generator ray is attained by a target generator after pullback.

theorem templateSymmetry_weight_ray_surjective
    (j : I) (hj : D.weight j ≠ 0) :
    ∃ (i : I) (s : ℝ), 0 < s ∧
      (D.weight i).comp A.val.toLinearMap = s • D.weight j := by
…

theorem OAI.PolycyclicRecognition.pulled_weight_ne_zero line 77

theorem OAI.PolycyclicRecognition.transformed_ray_trace_pos_multiple line 87

Source documentation

The actual positive multiplicities of the transformed ray quotient give a positive multiple of the source ray when pulled back.

theorem transformed_ray_trace_pos_multiple
    (hne : ∀ i, D.weight i ≠ 0) (j : I)
    (c : I → ℕ)
    (hout : ∀ i, (D.weight i).toContinuousLinearMap ∉
      transformedPolarCone (closedWeightRay (D.weight j).toContinuousLinearMap
        (by simpa using hne j)) A.val → c i = 0)
    (hin : ∀ i, (D.weight i).toContinuousLinearMap ∈
      transformedPolarCone (closedWeightRay (D.weight j).toContinuousLinearMap
        (by simpa using hne j)) A.val → 0 < c i) :
    ∃ r : ℝ, 0 < r ∧
      (∑ i, (c i : ℝ) • (D.weight i).toContinuousLinearMap).comp
        A.val.toLinearMap.toContinuousLinearMap = r • (D.weight j).toContinuousLinearMap := by
…

Mentions: OAI.PolycyclicRecognition.transformedPolarCone, OAI.PolycyclicRecognition.closedWeightRay

theorem OAI.PolycyclicRecognition.transformed_two_ray_trace_pos_coefficients line 127

Source documentation

For two independent source generators the transformed quotient trace has a strictly positive coefficient on each source extreme ray.

theorem transformed_two_ray_trace_pos_coefficients
    (hne : ∀ i, D.weight i ≠ 0) (j k : I)
    (hind : LinearIndependent ℝ
      ![(D.weight j).toContinuousLinearMap, (D.weight k).toContinuousLinearMap])
    (c : I → ℕ)
    (hout : ∀ i, (D.weight i).toContinuousLinearMap ∉
      transformedPolarCone (closedTwoWeightCone (D.weight j).toContinuousLinearMap
        (D.weight k).toContinuousLinearMap hind) A.val → c i = 0)
    (hin : ∀ i, (D.weight i).toContinuousLinearMap ∈
      transformedPolarCone (closedTwoWeightCone (D.weight j).toContinuousLinearMap
        (D.weight k).toContinuousLinearMap hind) A.val → 0 < c i) :
    ∃ r s : ℝ, 0 < r ∧ 0 < s ∧
…

Mentions: OAI.PolycyclicRecognition.transformedPolarCone, OAI.PolycyclicRecognition.closedTwoWeightCone