OAI/GroupTheory/PolycyclicRecognition/Analysis/SupportedAffineProbeSelection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_supported_affine_probe_sequence line 16

   Source documentation

   The supported compact-map comparison yields the actual pointwise bounds used on all the Cartan legs, with one tolerance for every probe.

   theorem exists_supported_affine_probe_sequence
       {X Z W V C : Type*} [Nonempty X] [MeasurableSpace X]
       [TopologicalSpace Z] [CompactSpace Z]
       [NormedAddCommGroup W] [NormedSpace ℝ W]
       [AddCommGroup V] [Module ℝ V] [Fintype C]
       [MeasurableSpace C(Z, W)] [BorelSpace C(Z, W)]
       [BorelSpace (C(Z, W) × C(Z, W))]
       [HasOuterApproxClosed (C(Z, W) × C(Z, W))]
       {Y : ℕ → Type*} [∀ n, TopologicalSpace (Y n)] [∀ n, CompactSpace (Y n)]
       [∀ n, T2Space (Y n)] [∀ n, MeasurableSpace (Y n)] [∀ n, BorelSpace (Y n)]
       [∀ n, Nonempty (Y n)]
       (μ : ProbabilityMeasure X) (ν : ∀ n, ProbabilityMeasure (Y n))
   …