OAI/GroupTheory/PolycyclicRecognition/Analysis/AffineSheetAgreement.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.affine_height_profiles_eq_of_open_agreement line 16

   Source documentation

   Agreement above any nonempty open set identifies both the label and the offset of affine height profiles. Surjectivity makes the height map open.

   theorem affine_height_profiles_eq_of_open_agreement
       {V W Z : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V]
       [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ W]
       [NormedAddCommGroup Z] [NormedSpace ℝ Z]
       (q : V →L[ℝ] W) (hq : Function.Surjective q)
       (A B : W →L[ℝ] Z) (b c : Z)
       (U O : Set V) (hO : IsOpen O) (hne : O.Nonempty) (hOU : O ⊆ U)
       (f g : V → Z)
       (hf : ∀ z ∈ U, f z = A (q z) + b) (hg : ∀ z ∈ U, g z = B (q z) + c)
       (heq : ∀ z ∈ O, f z = g z) :
       A = B ∧ b = c ∧ ∀ z ∈ U, f z = g z := by
   …

2. theorem OAI.PolycyclicRecognition.mem_support_map_of_continuous line 37

   Source documentation

   A continuous image of a supported sample is supported by its image law.

   theorem mem_support_map_of_continuous
       {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
       [MeasurableSpace X] [MeasurableSpace Y] [BorelSpace X] [BorelSpace Y]
       (μ : ProbabilityMeasure X) (f : X → Y) (hf : Continuous f)
       {x : X} (hx : x ∈ (μ : Measure X).support) :
       f x ∈ (ProbabilityMeasure.map μ f : Measure Y).support := by
   …

3. theorem OAI.PolycyclicRecognition.sampled_projection_tendsto line 54

   Source documentation

   Projection of a weak limit of sampled pairs is the weak limit of the projected samples, with no change of sampling law.

   theorem sampled_projection_tendsto
       {A X Y : Type*} [MeasurableSpace A]
       [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X]
       [TopologicalSpace Y] [MeasurableSpace Y] [BorelSpace Y]
       (μ : ℕ → ProbabilityMeasure A) (p : ℕ → A → X) (hp : ∀ n, Measurable (p n))
       (ν : ProbabilityMeasure X)
       (hν : Tendsto (fun n => ProbabilityMeasure.map (μ n) (p n)) atTop (𝓝 ν))
       (f : X → Y) (hf : Continuous f) :
       Tendsto (fun n => ProbabilityMeasure.map (μ n) (f ∘ p n)) atTop
         (𝓝 (ProbabilityMeasure.map ν f)) := by
   …

4. theorem OAI.PolycyclicRecognition.supported_profile_pair_eq_of_ae_discrepancy line 72

   Source documentation

   A uniform vanishing discrepancy for sampled profile pairs is inherited by every pair in the support of a weak limit.

   theorem supported_profile_pair_eq_of_ae_discrepancy
       {V W A : Type*} [TopologicalSpace V] [LocallyCompactSpace V]
       [PseudoMetricSpace W] [MeasurableSpace A]
       (S : Set C(V, W)) [MeasurableSpace (S × S)] [BorelSpace (S × S)]
       [HasOuterApproxClosed (S × S)]
       (samples : ℕ → ProbabilityMeasure A) (pair : ℕ → A → S × S)
       (hp : ∀ n, Measurable (pair n)) (ν : ProbabilityMeasure (S × S))
       (hν : Tendsto (fun n => ProbabilityMeasure.map (samples n) (pair n)) atTop (𝓝 ν))
       (z : V) (ε : ℕ → ℝ) (hε : Tendsto ε atTop (𝓝 0))
       (hbound : ∀ᶠ n in atTop, ∀ᵐ a ∂(samples n : Measure A),
         dist ((pair n a).1.val z) ((pair n a).2.val z) ≤ ε n)
       {f : S × S} (hf : f ∈ (ν : Measure (S × S)).support) :
   …

5. theorem OAI.PolycyclicRecognition.supported_profile_pair_eq_of_uniform_discrepancy line 98

   Source documentation

   Pointwise sample bounds imply the almost-everywhere version.

   theorem supported_profile_pair_eq_of_uniform_discrepancy
       {V W A : Type*} [TopologicalSpace V] [LocallyCompactSpace V]
       [PseudoMetricSpace W] [MeasurableSpace A]
       (S : Set C(V, W)) [MeasurableSpace (S × S)] [BorelSpace (S × S)]
       [HasOuterApproxClosed (S × S)]
       (samples : ℕ → ProbabilityMeasure A) (pair : ℕ → A → S × S)
       (hp : ∀ n, Measurable (pair n)) (ν : ProbabilityMeasure (S × S))
       (hν : Tendsto (fun n => ProbabilityMeasure.map (samples n) (pair n)) atTop (𝓝 ν))
       (z : V) (ε : ℕ → ℝ) (hε : Tendsto ε atTop (𝓝 0))
       (hbound : ∀ᶠ n in atTop, ∀ a,
         dist ((pair n a).1.val z) ((pair n a).2.val z) ≤ ε n)
       {f : S × S} (hf : f ∈ (ν : Measure (S × S)).support) :
   …