SourceBundleBlockPaths.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exact source-bundle boundaries and their individual paths

theorem OAI.PolycyclicRecognition.sampledBlockWord_source_product line 21

Source documentation

The product of each actual sampled block is its prescribed conjugated source-bundle product.

theorem sampledBlockWord_source_product {h m : ℕ}
    (lie : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) N)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) N → N)
    (X : I → L) (s : I → ℝ) (letters : Fin m → I) (r : ℝ)
    (φ : Fin h → N ≃* N) (sample : ℕ → ℝ → N)
    (hsample : ∀ (i : Fin h) (j : Fin m) t,
      sample (finProdFinEquiv (i, j)).val t = φ i
        (Exp (lie (t • (Real.exp (r * s (letters j)) • X (letters j))))))
    (t : Fin (h * m + h * m) → ℝ) (i : Fin h) :
    (sampledBlockWord sample t i).prod =
      φ i (sourceBundleProduct lie Exp X s letters (bundleParameterChart h m) r t i) := by
…

Mentions: OAI.PolycyclicRecognition.sampledBlockWord, OAI.PolycyclicRecognition.sourceBundleProduct, OAI.PolycyclicRecognition.bundleParameterChart

def OAI.PolycyclicRecognition.sourceBundleBoundary line 37
Source documentation
The prefix-defined boundary uses the same conjugated bundle increments as the Haar-preserving state-coordinate map.
```
def sourceBundleBoundary {h : ℕ} (n : N) (φ : Fin h → N ≃* N)
    (v : Fin h → N) (j : ℕ) : N :=
…
```
theorem OAI.PolycyclicRecognition.sourceBundleBoundary_zero line 42
theorem OAI.PolycyclicRecognition.sourceBundleBoundary_succ line 51
theorem OAI.PolycyclicRecognition.sourceBundleBoundary_eq_stateEquiv line 66
Source documentation
The paths' boundary coordinates coincide with the coordinates of the Haar-preserving source-state map.
```
theorem sourceBundleBoundary_eq_stateEquiv {h : ℕ} (n : N) (φ : Fin h → N ≃* N)
    (ψ : Fin h → N ≃ᵐ N) (hψ : ∀ i z, ψ i z = φ i z) (v : Fin h → N) (i : Fin h) :
    sourceBundleBoundary n φ v (i.val + 1) = sourceBundleStateEquiv h n ψ v i := by
…
```
Mentions: OAI.PolycyclicRecognition.sourceBundleBoundary, OAI.PolycyclicRecognition.sourceBundleStateEquiv
theorem OAI.PolycyclicRecognition.sampledBlockProducts_source_product line 76

theorem OAI.PolycyclicRecognition.successful_sourceBundle_block_path line 98

Source documentation

Each source bundle has a controlled path with its exact two boundary states, even when different bundles use different inner conjugations.

theorem successful_sourceBundle_block_path {h m : ℕ}
    (lie : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) N)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) N → N)
    (X : I → L) (s : I → ℝ) (letters : Fin m → I) (r : ℝ)
    (φ : Fin h → N ≃* N) (sample : ℕ → ℝ → N)
    (hsub : ∀ j u v, sample j u * (sample j v)⁻¹ = sample j (u - v))
    (hsample : ∀ (i : Fin h) (j : Fin m) t,
      sample (finProdFinEquiv (i, j)).val t = φ i
        (Exp (lie (t • (Real.exp (r * s (letters j)) • X (letters j))))))
    (ι : N →* G) (x d₀ : G) (A : Set N) (S : Set G) (i : Fin h)
    (d : Fin m → ℝ → G) (hd : ∀ j, Continuous (d j)) (hd₀ : ∀ j, d j 0 = 1)
    (hf : ∀ j : Fin m, Continuous (fun b => ι (sample (finProdFinEquiv (i, j)).val b)))
…