OAI/GroupTheory/PolycyclicRecognition/Analysis/AffineMeanApproximation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_affine_mean_approximation line 16

   Source documentation

   No point-mass choice is necessary: the first-moment argument selects an actual affine profile whenever the independent and affine errors vanish.

   theorem exists_affine_mean_approximation
       {S Z W L : Type*} [TopologicalSpace S] [CompactSpace S] [T2Space S]
       [SecondCountableTopology S] [MeasurableSpace S] [BorelSpace S]
       [TopologicalSpace Z] [CompactSpace Z] [NormedAddCommGroup W] [Nonempty L]
       (F : S → C(Z, W)) (hF : Continuous F) (A : L → C(Z, W))
       (μ : ℕ → ProbabilityMeasure S)
       (hpair : ∀ ε : ℝ, 0 < ε → Tendsto (fun n =>
         (μ n : Measure S).prod (μ n : Measure S) {p | ε ≤ dist (F p.1) (F p.2)})
           atTop (𝓝 0))
       (haffine : ∀ ε : ℝ, 0 < ε → Tendsto (fun n =>
         (μ n : Measure S) {x | ε ≤ infDist (F x) (affineProfileClass A)})
           atTop (𝓝 0)) :
   …

   Mentions: OAI.PolycyclicRecognition.affineProfileClass

2. theorem OAI.PolycyclicRecognition.affine_profiles_offset_dist_le line 43

   Source documentation

   Pointwise cancellation controls the distance between affine offsets.

   theorem affine_profiles_offset_dist_le
       {Z W : Type*} [TopologicalSpace Z] [CompactSpace Z] [NormedAddCommGroup W]
       (A : C(Z, W)) (b c : W) :
       dist (A + ContinuousMap.const Z b) (A + ContinuousMap.const Z c) ≤ dist b c := by
   …

3. theorem OAI.PolycyclicRecognition.mean_affine_offset_dist_le line 53

   Source documentation

   Evaluation and the norm integral inequality control the change of offset.

   theorem mean_affine_offset_dist_le
       {S Z W : Type*} [TopologicalSpace S] [CompactSpace S]
       [MeasurableSpace S] [BorelSpace S] [TopologicalSpace Z] [CompactSpace Z]
       [NormedAddCommGroup W] [NormedSpace ℝ W] [CompleteSpace W]
       (F : S → C(Z, W)) (hF : Continuous F) (A : C(Z, W))
       (z₀ : Z) (hA : A z₀ = 0) (b : W) (μ : ProbabilityMeasure S) :
       dist b (∫ y, F y z₀ ∂(μ : Measure S)) ≤
         ∫ x, dist (F x) (A + ContinuousMap.const Z b) ∂(μ : Measure S) := by
   …

4. theorem OAI.PolycyclicRecognition.mean_normalized_affine_error_le line 89

   Source documentation

   Replacing an approximate affine offset by the mean value at the identity increases the mean error by at most a factor of two.

   theorem mean_normalized_affine_error_le
       {S Z W : Type*} [TopologicalSpace S] [CompactSpace S]
       [MeasurableSpace S] [BorelSpace S]
       [TopologicalSpace Z] [CompactSpace Z]
       [NormedAddCommGroup W] [NormedSpace ℝ W] [CompleteSpace W]
       (F : S → C(Z, W)) (hF : Continuous F) (A : C(Z, W))
       (z₀ : Z) (hA : A z₀ = 0) (b : W) (μ : ProbabilityMeasure S) :
       (∫ x, dist (F x) (A + ContinuousMap.const Z
         (∫ y, F y z₀ ∂(μ : Measure S))) ∂(μ : Measure S)) ≤
         2 * ∫ x, dist (F x) (A + ContinuousMap.const Z b) ∂(μ : Measure S) := by
   …

5. theorem OAI.PolycyclicRecognition.exists_mean_normalized_affine_approximation line 119

   Source documentation

   The deterministic offset is exactly the mean height at the identity.

   theorem exists_mean_normalized_affine_approximation
       {S Z W L : Type*} [TopologicalSpace S] [CompactSpace S] [T2Space S]
       [SecondCountableTopology S] [MeasurableSpace S] [BorelSpace S]
       [TopologicalSpace Z] [CompactSpace Z]
       [NormedAddCommGroup W] [NormedSpace ℝ W] [CompleteSpace W] [Nonempty L]
       (F : S → C(Z, W)) (hF : Continuous F) (A : L → C(Z, W))
       (z₀ : Z) (hA : ∀ a, A a z₀ = 0) (μ : ℕ → ProbabilityMeasure S)
       (hpair : ∀ ε : ℝ, 0 < ε → Tendsto (fun n =>
         (μ n : Measure S).prod (μ n : Measure S) {p | ε ≤ dist (F p.1) (F p.2)})
           atTop (𝓝 0))
       (haffine : ∀ ε : ℝ, 0 < ε → Tendsto (fun n =>
         (μ n : Measure S) {x | ε ≤ infDist (F x) (affineProfileClass A)})
   …

   Mentions: OAI.PolycyclicRecognition.affineProfileClass