SuccessfulSampleBlockPaths.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Separate geometric paths for successive sampled bundles

def OAI.PolycyclicRecognition.sampledBlockWord line 16
Source documentation
The actual difference word of one block of the global sample vector.
```
def sampledBlockWord {h m : ℕ} (sample : ℕ → ℝ → N)
    (t : Fin (h * m + h * m) → ℝ) (i : Fin h) : List N :=
…
```
def OAI.PolycyclicRecognition.sampledBlockProducts line 23
Source documentation
Products of complete sampled blocks, extended by the identity.
```
def sampledBlockProducts {h m : ℕ} (sample : ℕ → ℝ → N)
    (t : Fin (h * m + h * m) → ℝ) (j : ℕ) : N :=
…
```

theorem OAI.PolycyclicRecognition.successful_sample_block_path line 31

Source documentation

A single block inherits successful sheets from the global coupled sample. Its geometric path may use a block-specific template.

theorem successful_sample_block_path {h m : ℕ}
    (ι : N →* G) (x d₀ : G) (A : Set N) (S : Set G)
    (sample : ℕ → ℝ → N)
    (hsub : ∀ j s t, sample j s * (sample j t)⁻¹ = sample j (s - t))
    (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)))
    (hf₀ : ∀ j : Fin m, ι (sample (finProdFinEquiv (i, j)).val 0) = 1)
    (r : ℝ) {L κ ρ : ℝ} (hL : 0 ≤ L) (hκ : 0 ≤ κ)
    (hbase : ∀ n ∈ A, x * ι n * d₀ ∈ S)
    (hstep : ∀ n ∈ A, ∀ j : Fin m, ∀ b : ℝ, |b| ≤ 2 * ρ →
      n * sample (finProdFinEquiv (i, j)).val b ∈ A →
…