OAI/GroupTheory/PolycyclicRecognition/Analysis/ProfileLawProduct.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.probability_map_prod_apply line 12

   Source documentation

   Independent pushforward samples have the pushed-forward product law.

   theorem probability_map_prod_apply
       {X S : Type*} [MeasurableSpace X] [MeasurableSpace S]
       (μ : ProbabilityMeasure X) (f : X → S) (hf : Measurable f)
       (B : Set (S × S)) (hB : MeasurableSet B) :
       (ProbabilityMeasure.map μ f : Measure S).prod
         (ProbabilityMeasure.map μ f : Measure S) B =
         (μ : Measure X).prod (μ : Measure X) ((Prod.map f f) ⁻¹' B) := by
   …

2. theorem OAI.PolycyclicRecognition.probability_map_pair_distance_of_ae_eq line 25

   Source documentation

   Representatives agreeing almost everywhere induce exactly the same pairwise distance probabilities.

   theorem probability_map_pair_distance_of_ae_eq
       {X S Y : Type*} [MeasurableSpace X] [MeasurableSpace S]
       [PseudoMetricSpace Y]
       (μ : ProbabilityMeasure X) (f : X → S) (hf : Measurable f)
       (F : S → Y) (raw : X → Y) (heq : ∀ᵐ x ∂(μ : Measure X), F (f x) = raw x)
       (η : ℝ) (hB : MeasurableSet {p : S × S | η ≤ dist (F p.1) (F p.2)}) :
       (ProbabilityMeasure.map μ f : Measure S).prod
         (ProbabilityMeasure.map μ f : Measure S) {p | η ≤ dist (F p.1) (F p.2)} =
         (μ : Measure X).prod (μ : Measure X) {p | η ≤ dist (raw p.1) (raw p.2)} := by
   …