TemplateOffsetCones.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The finite family of polar quotients that detects one root offset

def OAI.PolycyclicRecognition.rootOffsetConeIndex line 20
Source documentation
One ray, and the two-ray cones independent of that ray. This is precisely the finite family needed for a single neighboring root step.
```
def rootOffsetConeIndex (D : SupportDatum W I B) (j : I) :=
…
```
Mentions: OAI.PolycyclicRecognition.SupportDatum
instance OAI.PolycyclicRecognition.(instance at line 24) line 24
instance OAI.PolycyclicRecognition.(instance at line 28) line 28

def OAI.PolycyclicRecognition.rootOffsetCone line 31

Source documentation

The source polar cone attached to one member of the finite family.

def rootOffsetCone (D : SupportDatum W I B) (hne : ∀ i, D.weight i ≠ 0) (j : I) :
    rootOffsetConeIndex D j → ProperCone ℝ (StrongDual ℝ W)
  | none => closedWeightRay (D.weight j).toContinuousLinearMap (by simpa using hne j)
  | some k => closedTwoWeightCone (D.weight j).toContinuousLinearMap
      (D.weight k.val).toContinuousLinearMap k.property

Mentions: OAI.PolycyclicRecognition.SupportDatum, OAI.PolycyclicRecognition.rootOffsetConeIndex, OAI.PolycyclicRecognition.closedWeightRay, OAI.PolycyclicRecognition.closedTwoWeightCone

theorem OAI.PolycyclicRecognition.rootOffsetCone_salient line 37
theorem OAI.PolycyclicRecognition.weight_mem_rootOffsetCone line 44

theorem OAI.PolycyclicRecognition.exists_uniform_rootOffsetCone_threshold line 59

Source documentation

Source enlargement and bridge error can be fixed before the affine label is selected, simultaneously for all quotients used by this root.

theorem exists_uniform_rootOffsetCone_threshold
    (D : SupportDatum W I B) (j : I)
    (target : templateSymmetryGroup D → rootOffsetConeIndex D j → ℝ)
    (htarget : ∀ A s, 0 < target A s)
    {source A B Λ c : ℝ} (hsource : 0 < source)
    (hA : 0 ≤ A) (hB : 0 ≤ B) (hΛ : 0 ≤ Λ) (hc : 0 ≤ c) :
    ∃ δ₀ ε : ℝ, 0 < δ₀ ∧ 0 < ε ∧ δ₀ ≤ source ∧
      ∀ δ : ℝ, 0 < δ → δ ≤ δ₀ → c * δ ≤ 1 ∧
        ∀ L s, Λ * (A * δ + B * ε) ≤ target L s := by
…

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

theorem OAI.PolycyclicRecognition.eq_of_rootOffsetCone_trace_inequalities line 83

Source documentation

Forward and reverse volume inequalities for this finite family force the two offsets to coincide. Each inequality uses its own actual quotient trace, with positive multiplicity exactly on the transformed cone.

theorem eq_of_rootOffsetCone_trace_inequalities
    (D : SupportDatum W I B) (A : templateSymmetryGroup D)
    (hne : ∀ i, D.weight i ≠ 0) (j : I)
    (c : rootOffsetConeIndex D j → I → ℕ)
    (hout : ∀ s i, (D.weight i).toContinuousLinearMap ∉
      transformedPolarCone (rootOffsetCone D hne j s) A.val → c s i = 0)
    (hin : ∀ s i, (D.weight i).toContinuousLinearMap ∈
      transformedPolarCone (rootOffsetCone D hne j s) A.val → 0 < c s i)
    (x y : W)
    (hf : ∀ s, (∑ i, (c s i : ℝ) • (D.weight i).toContinuousLinearMap) (y - x) ≤ 0)
    (hr : ∀ s, (∑ i, (c s i : ℝ) • (D.weight i).toContinuousLinearMap) (x - y) ≤ 0) :
    x = y := by
…

Mentions: OAI.PolycyclicRecognition.SupportDatum, OAI.PolycyclicRecognition.templateSymmetryGroup, OAI.PolycyclicRecognition.rootOffsetConeIndex, OAI.PolycyclicRecognition.transformedPolarCone, OAI.PolycyclicRecognition.rootOffsetCone