OAI/GroupTheory/PolycyclicRecognition/Analysis/ProfileLawIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.integral_profile_value_map line 13

   Source documentation

   Push a continuous observable through the profile law and use the actual sample formula, which need only hold almost everywhere.

   theorem integral_profile_value_map
       {X S W : Type*} [MeasurableSpace X] [MeasurableSpace S]
       [TopologicalSpace S] [BorelSpace S]
       [NormedAddCommGroup W] [NormedSpace ℝ W] [SecondCountableTopology W]
       (μ : ProbabilityMeasure X) (f : X → S) (hf : Measurable f)
       (obs : S → W) (hobs : Continuous obs) (raw : X → W)
       (heq : ∀ᵐ x ∂(μ : Measure X), obs (f x) = raw x) :
       (∫ y, obs y ∂(ProbabilityMeasure.map μ f : Measure S)) =
         ∫ x, raw x ∂(μ : Measure X) := by
   …

2. theorem OAI.PolycyclicRecognition.integral_profile_distance_map line 27

   Source documentation

   Uniform-distance means are unchanged by replacing compact profile representatives with their original almost-everywhere values.

   theorem integral_profile_distance_map
       {X S Y : Type*} [MeasurableSpace X] [MeasurableSpace S]
       [TopologicalSpace S] [BorelSpace S] [PseudoMetricSpace Y]
       (μ : ProbabilityMeasure X) (f : X → S) (hf : Measurable f)
       (obs : S → Y) (hobs : Continuous obs) (raw : X → Y)
       (heq : ∀ᵐ x ∂(μ : Measure X), obs (f x) = raw x) (y : Y) :
       (∫ z, dist (obs z) y ∂(ProbabilityMeasure.map μ f : Measure S)) =
         ∫ x, dist (raw x) y ∂(μ : Measure X) := by
   …