ProfileParameterContinuity.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Continuous dependence of actual profiles on their sheet parameters

def OAI.PolycyclicRecognition.rescaledContinuousProfile line 16
Source documentation
The actual rescaled profile as a continuous function of the chart point.
```
def rescaledContinuousProfile (J : G → W) (hJ : Continuous J)
    (x k : G) (r : ℝ) (φ : Z → G) (hφ : Continuous φ) : C(Z, W) :=
…
```
theorem OAI.PolycyclicRecognition.continuous_rescaledContinuousProfile line 22
Source documentation
At a fixed scale the full profile varies continuously with its suffix, for the topology of uniform convergence on compact chart sets.
```
theorem continuous_rescaledContinuousProfile
    (J : G → W) (hJ : Continuous J) (x : G) (r : ℝ)
    (φ : Z → G) (hφ : Continuous φ) :
    Continuous (fun k => rescaledContinuousProfile J hJ x k r φ hφ) := by
…
```
Mentions: OAI.PolycyclicRecognition.rescaledContinuousProfile

theorem OAI.PolycyclicRecognition.continuous_sampled_profile_subtype line 33

Source documentation

Restricting to a compact profile family preserves the continuity of actual sheet sampling. The membership proof does not choose a new profile.

theorem continuous_sampled_profile_subtype
    (J : G → W) (hJ : Continuous J) (x : G) (r : ℝ)
    (φ : Z → G) (hφ : Continuous φ) (suffix : A → G) (hsuffix : Continuous suffix)
    (S : Set C(Z, W))
    (hmem : ∀ a, rescaledContinuousProfile J hJ x (suffix a) r φ hφ ∈ S) :
    Continuous (fun a => (⟨rescaledContinuousProfile J hJ x (suffix a) r φ hφ,
      hmem a⟩ : S)) :=
…

Mentions: OAI.PolycyclicRecognition.rescaledContinuousProfile

theorem OAI.PolycyclicRecognition.exists_measurable_sampled_profile line 44

Source documentation

Profiles are extended measurably off the sampling cell. Their source formula is required only on that cell, where compact containment is known.

theorem exists_measurable_sampled_profile
    [MeasurableSpace A] [BorelSpace A]
    (J : G → W) (hJ : Continuous J) (x : G) (r : ℝ)
    (φ : Z → G) (hφ : Continuous φ) (suffix : A → G) (hsuffix : Continuous suffix)
    (C : Set A) (hC : MeasurableSet C) (hne : C.Nonempty)
    (S : Set C(Z, W)) [MeasurableSpace S] [BorelSpace S]
    (hmem : ∀ a ∈ C, rescaledContinuousProfile J hJ x (suffix a) r φ hφ ∈ S) :
    ∃ profile : A → S, Measurable profile ∧ ∀ a ∈ C, ∀ z,
      (profile a).val z = rescaledMapProfile J x (suffix a) r φ z := by
…

Mentions: OAI.PolycyclicRecognition.rescaledContinuousProfile, OAI.PolycyclicRecognition.rescaledMapProfile

theorem OAI.PolycyclicRecognition.exists_measurable_profile_chain line 68

Source documentation

A finite family of actual sheet suffixes gives measurable profile chains on a carrying cell. All choices remain exact on that cell.

theorem exists_measurable_profile_chain
    [MeasurableSpace A] [BorelSpace A] {N : ℕ}
    (J : ℕ → G → W) (hJ : ∀ n, Continuous (J n)) (x : ℕ → G) (r : ℕ → ℝ)
    (φ : ℕ → Z → G) (hφ : ∀ n, Continuous (φ n))
    (suffix : ℕ → Fin (N + 1) → A → G) (hsuffix : ∀ n j, Continuous (suffix n j))
    (C : Set A) (hC : MeasurableSet C) (hne : C.Nonempty)
    (S : Set C(Z, W)) [MeasurableSpace S] [BorelSpace S]
    (hmem : ∀ n j a, a ∈ C → ∃ f ∈ S, ∀ z,
      f z = rescaledMapProfile (J n) (x n) (suffix n j a) (r n) (φ n) z) :
    ∃ profile : ℕ → A → Fin (N + 1) → S, (∀ n, Measurable (profile n)) ∧
      ∀ n a j, a ∈ C → ∀ z,
      (profile n a j).val z = rescaledMapProfile (J n) (x n) (suffix n j a) (r n) (φ n) z := by
…

Mentions: OAI.PolycyclicRecognition.rescaledMapProfile