OAI/GroupTheory/PolycyclicRecognition/Analysis/MeasurableProbeProfiles.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_measurable_borel_sampled_profile line 19

   Source documentation

   A Borel suffix selector gives a Borel profile in the fixed compact profile family, with the actual formula on the carrying sample cell.

   theorem exists_measurable_borel_sampled_profile
       {A : Type*} [MeasurableSpace A]
       (J : G → W) (hJ : Continuous J) (x : G) (r : ℝ)
       (φ : Z → G) (hφ : Continuous φ) (suffix : A → G) (hsuffix : Measurable suffix)
       (C : Set A) (hC : MeasurableSet C) (hne : C.Nonempty)
       (S : Set C(Z, W))
       (hmem : ∀ a ∈ C, rescaledContinuousProfile J hJ x (suffix a) r φ hφ ∈ S) :
       ∃ profile : A → S, Measurable profile ∧ ∀ a ∈ C, ∀ z,
         (profile a).val z = rescaledMapProfile J x (suffix a) r φ z := by
   …

   Mentions: OAI.PolycyclicRecognition.rescaledContinuousProfile, OAI.PolycyclicRecognition.rescaledMapProfile

2. theorem OAI.PolycyclicRecognition.exists_measurable_probe_profile_chain line 44

   Source documentation

   At every scale, finitely many Borel-selected prefixes have measurable representatives in the same profile family. The probe spaces may vary with the ideal box; no continuity of the tile selector is required.

   theorem exists_measurable_probe_profile_chain
       {A : ℕ → Type*} [∀ n, MeasurableSpace (A n)] {N : ℕ}
       (J : ℕ → G → W) (hJ : ∀ n, Continuous (J n)) (x : ℕ → G) (r : ℕ → ℝ)
       (φ : ℕ → Z → G) (hφ : ∀ n, Continuous (φ n))
       (suffix : ∀ n, Fin (N + 1) → A n → G) (hsuffix : ∀ n j, Measurable (suffix n j))
       (C : ∀ n, Set (A n)) (hC : ∀ n, MeasurableSet (C n)) (hne : ∀ n, (C n).Nonempty)
       (S : Set C(Z, W))
       (hmem : ∀ n j a, a ∈ C n → ∃ f ∈ S, ∀ z,
         f z = rescaledMapProfile (J n) (x n) (suffix n j a) (r n) (φ n) z) :
       ∃ profile : ∀ n, A n → Fin (N + 1) → S, (∀ n, Measurable (profile n)) ∧
         ∀ n a j, a ∈ C n → ∀ z,
         (profile n a j).val z = rescaledMapProfile (J n) (x n) (suffix n j a) (r n) (φ n) z := by
   …

   Mentions: OAI.PolycyclicRecognition.rescaledMapProfile