OAI/Dynamics/SmoothObstruction/Selection.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothObstruction.CanonicalRelation.measurable_solution line 24

   Source documentation

   A Borel relation with exactly one output at every input has a genuine measurable solution map. Its definition does not depend on any auxiliary frame certificate used to obtain existence and uniqueness.

   theorem measurable_solution (R : Set (X × Y)) (hR : MeasurableSet R)
       (hex : ∀ x,∃! y,(x,y)∈R) :
       ∃ f : X → Y,Measurable f ∧ (∀ x,(x,f x)∈R) ∧
         ∀ x y,(x,y)∈R → y=f x := by
   …

2. theorem OAI.SmoothObstruction.CanonicalRelation.retained_solution line 48

   Source documentation

   The retained set has its original Borel subspace, not a conditioned probability space. The measurable total extension is only for convenient pushforward notation; it is equal to the canonical solution on the carrier.

   theorem retained_solution [Nonempty Y] (G : Set X) (hG : MeasurableSet G)
       (R : X → Y → Prop) (hR : MeasurableSet {z : X×Y | z.1∈G ∧ R z.1 z.2})
       (hex : ∀ x∈G,∃! y,R x y) :
       ∃ f : X → Y,Measurable f ∧ (∀ x∈G,R x (f x)) ∧
         ∀ x∈G,∀ y,R x y → y=f x := by
   …

3. theorem OAI.SmoothObstruction.CanonicalRelation.local_derivative line 87

   Source documentation

   Local analytic branches agree with the canonical Borel solution merely by satisfying its boundary relation inside the uniqueness tube. The frame witnesses and chart codes need not be continuous functions of the inputs.

   theorem local_derivative (G : Set E) (x : E) (hx : x∈G)
       (R : E → F → Prop) (f g : E → F) (L : E →L[ℝ] F)
       (hu : ∀ u∈G,∀ v,R u v → v=f u)
       (hg : HasFDerivAt g L x) (hrel : ∀ᶠ u in 𝓝[G] x,R u (g u)) :
       HasFDerivWithinAt f L G x := by
   …

4. def OAI.SmoothObstruction.SelectedTube.tube line 106

   Source documentation

   The literal fixed-atlas coordinate tube, with chart sources checked. Only the base point chooses the chart; the second point need not be good.

   def tube (q : X → C) (U : C → Set X) (φ : C → X → E)
       (f : ℕ → X → X) (n : ℕ) (δ : ℝ) (x z : X) : Prop :=
   …

5. lemma OAI.SmoothObstruction.SelectedTube.measurable_evaluate line 112
6. lemma OAI.SmoothObstruction.SelectedTube.measurable_tube line 116
7. def OAI.SmoothObstruction.MeasurableSwitch.relation line 147

   Source documentation

   Fixed-bin future/past observations and the two old coordinate tubes. All auxiliary frames have disappeared from this boundary relation.

   def relation (F P : X → X → E) (TF TB : X → X → Prop) (u : X×X) (z : X) : Prop :=
   …

8. lemma OAI.SmoothObstruction.MeasurableSwitch.measurable_relation line 150
9. theorem OAI.SmoothObstruction.MeasurableSwitch.canonical_pair line 170

   Source documentation

   The original retained carrier gives one globally measurable pair map. There is no measurable moving-frame selection and no conditioning of a law. Existence and uniqueness are supplied by the actual finite-tube solve.

   theorem canonical_pair [StandardBorelSpace X] [Nonempty X]
       (G : Set (X×X)) (hG : MeasurableSet G)
       (F P : X → X → E) (hF : Measurable (Function.uncurry F))
       (hP : Measurable (Function.uncurry P))
       (TF TB : X → X → Prop) (hTF : MeasurableSet {p : X×X | TF p.1 p.2})
       (hTB : MeasurableSet {p : X×X | TB p.1 p.2})
       (hex : ∀ u∈G,∃! z,relation F P TF TB u z)
       (hex' : ∀ u∈G,∃! w,relation F P TF TB u.swap w) :
       ∃ Φ : X×X → X×X,Measurable Φ ∧
         (∀ u∈G,relation F P TF TB u (Φ u).1 ∧ relation F P TF TB u.swap (Φ u).2) ∧
         (∀ u∈G,∀ z,relation F P TF TB u z → z=(Φ u).1) ∧
         (∀ u∈G,∀ w,relation F P TF TB u.swap w → w=(Φ u).2) := by
   …

   Mentions: OAI.SmoothObstruction.MeasurableSwitch.relation

10. def OAI.SmoothObstruction.EndpointObservation.observation line 205

    Source documentation

    The source endpoint observation in the ambient coordinate space. Its finite index consists ONLY of the starting coarse bin and endpoint coarse bin; an internal frame witness is not part of this index.

    def observation (c : X → C) (b : X → B) (f : X → X)
        (φ : B → X → E) (P : C → B → E →L[ℝ] E) (x z : X) : E :=
    …

11. lemma OAI.SmoothObstruction.EndpointObservation.measurable_observation line 209
12. lemma OAI.SmoothObstruction.EndpointObservation.observation_fixed line 227

    Source documentation

    Positive bin margins turn the ambient observations into the actual fixed smooth endpoint maps on a neighborhood; there is no differentiability claim for the discontinuously selected observation itself.

    lemma observation_fixed (c : X → C) (b : X → B) (f : X → X)
        (φ : B → X → E) (P : C → B → E →L[ℝ] E)
        (x y z : X) (hc : c x=c y) (hb : b (f x)=b (f y)) :
        observation c b f φ P x z=observation c b f φ P y z := by
    …

    Mentions: OAI.SmoothObstruction.EndpointObservation.observation

13. lemma OAI.SmoothObstruction.EndpointObservation.observation_eq_iff line 233
14. def OAI.SmoothObstruction.ManifoldCoordinates.borelChart line 249

    Source documentation

    A chart has no prescribed behaviour outside its source. This Borel extension, used only to state global relations, agrees with it on the source.

    noncomputable def borelChart (a : M) : M → EuclideanSpace ℝ (Fin d) := by
    …

15. lemma OAI.SmoothObstruction.ManifoldCoordinates.borelChart_eq line 253
16. lemma OAI.SmoothObstruction.ManifoldCoordinates.measurable_borelChart line 260
17. lemma OAI.SmoothObstruction.ManifoldCoordinates.measurable_originalTube line 269
18. def OAI.SmoothObstruction.ManifoldCoordinates.originalObservation line 287
19. lemma OAI.SmoothObstruction.ManifoldCoordinates.measurable_originalObservation line 292
20. lemma OAI.SmoothObstruction.ManifoldCoordinates.originalObservation_eq_iff line 304
21. lemma OAI.SmoothObstruction.ManifoldCoordinates.originalTube_mono line 312
22. theorem OAI.SmoothObstruction.ManifoldCoordinates.canonical_original_switch line 330

    Source documentation

    A measurable, witness-independent ORIGINAL pair switch. Its Borel relation uses zero-extended charts, but all asserted equations and tube estimates are in the original atlas. The retained set has not been normalized or repartitioned.

    theorem canonical_original_switch (hclosed : IsClosed (range I))
        (S : Diffeomorph I I M M ∞) (a : ι → M) (K : ι → Set M)
        (hK : ∀ i,IsCompact (K i)) (hKU : ∀ i,K i⊆(chartAt H (a i)).source) :
        ∃ r₀ C₀ : ℝ,0<r₀ ∧ 1≤C₀ ∧
          ∀ (C J : Type*) [Fintype C] [MeasurableSpace C] [MeasurableSingletonClass C]
            [Fintype J] [MeasurableSpace J] [MeasurableSingletonClass J]
            (c : M → ι) (P : M → C) (L : M → J) (G R : Set M)
            (n : ℕ) (B R₀ ε g α r δ : ℝ) (γ : C → ℝ)
            (A : ∀ x:G,BilateralGauge I S a c n B R₀ x)
            (T : G → Finset (Fin d)) (ref : G → G)
            (Wf Wb : C×C → Submodule ℝ (EuclideanSpace ℝ (Fin d))),
            Measurable c → Measurable P → Measurable L → MeasurableSet R → R⊆G →
    …

    Mentions: OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge

23. theorem OAI.SmoothObstruction.ManifoldCoordinates.canonical_original_switch_unique line 493

    Source documentation

    A measurable, witness-independent ORIGINAL pair switch. Its Borel relation uses zero-extended charts, but all asserted equations and tube estimates are in the original atlas. The retained set has not been normalized or repartitioned.

    theorem canonical_original_switch_unique (hclosed : IsClosed (range I))
        (S : Diffeomorph I I M M ∞) (a : ι → M) (K : ι → Set M)
        (hK : ∀ i,IsCompact (K i)) (hKU : ∀ i,K i⊆(chartAt H (a i)).source) :
        ∃ r₀ C₀ : ℝ,0<r₀ ∧ 1≤C₀ ∧
          ∀ (C J : Type*) [Fintype C] [MeasurableSpace C] [MeasurableSingletonClass C]
            [Fintype J] [MeasurableSpace J] [MeasurableSingletonClass J]
            (c : M → ι) (P : M → C) (L : M → J) (G R : Set M)
            (n : ℕ) (B R₀ ε g α r δ : ℝ) (γ : C → ℝ)
            (A : ∀ x:G,BilateralGauge I S a c n B R₀ x)
            (T : G → Finset (Fin d)) (ref : G → G)
            (Wf Wb : C×C → Submodule ℝ (EuclideanSpace ℝ (Fin d))),
            Measurable c → Measurable P → Measurable L → MeasurableSet R → R⊆G →
    …

    Mentions: OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge

24. theorem OAI.SmoothObstruction.ManifoldCoordinates.canonical_original_switch_complete line 663

    Source documentation

    A measurable, witness-independent ORIGINAL pair switch. Its Borel relation uses zero-extended charts, but all asserted equations and tube estimates are in the original atlas. The retained set has not been normalized or repartitioned.

    theorem canonical_original_switch_complete (hclosed : IsClosed (range I))
        (S : Diffeomorph I I M M ∞) (a : ι → M) (K : ι → Set M)
        (hK : ∀ i,IsCompact (K i)) (hKU : ∀ i,K i⊆(chartAt H (a i)).source) :
        ∃ r₀ C₀ : ℝ,0<r₀ ∧ 1≤C₀ ∧
          ∀ (C J : Type*) [Fintype C] [MeasurableSpace C] [MeasurableSingletonClass C]
            [Fintype J] [MeasurableSpace J] [MeasurableSingletonClass J]
            (c : M → ι) (P : M → C) (L : M → J) (G R : Set M)
            (n : ℕ) (B R₀ ε g α r δ : ℝ) (γ : C → ℝ)
            (A : ∀ x:G,BilateralGauge I S a c n B R₀ x)
            (T : G → Finset (Fin d)) (ref : G → G)
            (Wf Wb : C×C → Submodule ℝ (EuclideanSpace ℝ (Fin d))),
            Measurable c → Measurable P → Measurable L → MeasurableSet R → R⊆G →
    …

    Mentions: OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge