NeighborProfileGluing.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

A single profile on the two cells of a neighboring pair

def OAI.PolycyclicRecognition.glueNeighborProfile line 18
Source documentation
Retain the first profile on the first cell and the transported second profile elsewhere. Compatibility makes the values agree on the overlap.
```
def glueNeighborProfile (A : Set N) (t : N) (f : N → S × S) (x : N) : S := by
…
```
theorem OAI.PolycyclicRecognition.measurable_glueNeighborProfile line 24
theorem OAI.PolycyclicRecognition.glueNeighborProfile_pair line 31

theorem OAI.PolycyclicRecognition.glueNeighborProfile_actual line 47

Source documentation

Injective evaluation into actual profiles supplies overlap compatibility and the correct value throughout the union of the neighboring cells.

theorem glueNeighborProfile_actual {A : Set N} (t : N) (f : N → S × S)
    (value : S → V) (hvalue : Function.Injective value) (actual : N → V)
    (hfirst : ∀ x ∈ A, value (f x).1 = actual x)
    (hsecond : ∀ x ∈ A, value (f x).2 = actual (x * t)) :
    (∀ x ∈ A, (glueNeighborProfile A t f x,
      glueNeighborProfile A t f (x * t)) = f x) ∧
    ∀ x ∈ A ∪ (fun y => y * t) '' A,
      value (glueNeighborProfile A t f x) = actual x := by
…

Mentions: OAI.PolycyclicRecognition.glueNeighborProfile

theorem OAI.PolycyclicRecognition.map_glueNeighborProfile_pair line 67

Source documentation

Gluing preserves the original joint probability law exactly.

theorem map_glueNeighborProfile_pair (μ : ProbabilityMeasure N)
    {A : Set N} (t : N) (f : N → S × S)
    (hμ : ∀ᵐ x ∂(μ : Measure N), x ∈ A)
    (hcompat : ∀ x ∈ A, x * t ∈ A → (f (x * t)).1 = (f x).2) :
    ProbabilityMeasure.map μ
      (fun x => (glueNeighborProfile A t f x, glueNeighborProfile A t f (x * t))) =
      ProbabilityMeasure.map μ f := by
…

Mentions: OAI.PolycyclicRecognition.glueNeighborProfile