Models.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SmoothObstruction.ConullConjugate line 14
Source documentation
Measurable conjugacy on invariant conull measurable subsets, not a continuous conjugacy and not merely a factor map.
Also declared: ComparatorChallenges/SmoothObstruction.lean:45 (same declaration text).
```
def ConullConjugate {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
    (μ : Measure X) (T : X → X) (ν : Measure Y) (S : Y → Y) : Prop :=
…
```
def OAI.SmoothObstruction.SmoothPositiveDensity line 26
Source documentation
Positive smooth local coordinate densities. In a half-space chart, ContDiffOn includes smoothness up to the boundary. Absolute Lebesgue density is used; no orientation or volume form is part of the data.
Also declared: ComparatorChallenges/SmoothObstruction.lean:57 (same declaration text).
```
def SmoothPositiveDensity {d : ℕ} {H : Type*} [TopologicalSpace H]
    (I : ModelWithCorners ℝ (EuclideanSpace ℝ (Fin d)) H)
    {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [MeasurableSpace M]
    (ν : Measure M) : Prop :=
…
```
def OAI.SmoothObstruction.HasModelWith line 39
Source documentation
A smooth positive-volume model with a specified Euclidean or half-space manifold model. All model dimensions will be quantified below.
Also declared: ComparatorChallenges/SmoothObstruction.lean:70 (same declaration text).
```
def HasModelWith {X : Type*} [MeasurableSpace X]
    (μ : Measure X) (T : X → X) {d : ℕ} {H : Type} [TopologicalSpace H]
    (I : ModelWithCorners ℝ (EuclideanSpace ℝ (Fin d)) H) : Prop :=
…
```
def OAI.SmoothObstruction.HasSmoothPositiveVolumeModel line 53
Source documentation
Closed manifolds of all dimensions (including zero), and smooth manifolds with boundary of every positive finite dimension. Nonorientable manifolds are included: no orientability hypothesis occurs.
Also declared: ComparatorChallenges/SmoothObstruction.lean:84 (same declaration text).
```
def HasSmoothPositiveVolumeModel {X : Type*} [MeasurableSpace X]
    (μ : Measure X) (T : X → X) : Prop :=
…
```
def OAI.SmoothObstruction.ConullTransport.inverse line 67
Source documentation
A measurable total representative of the inverse conjugacy; it uses an arbitrary value only off the given invariant conull subset.
```
noncomputable def inverse (A : Set X) (B : Set Y) (e : A ≃ᵐ B) (x₀ : X) : Y → X :=
…
```
lemma OAI.SmoothObstruction.ConullTransport.inverse_coe line 70
lemma OAI.SmoothObstruction.ConullTransport.measurable_inverse line 74

theorem OAI.SmoothObstruction.ConullTransport.preserving_inverse line 81

Source documentation

The arbitrary extension still pushes the full original probability measure to exactly μ. No normalization or exceptional-set approximation.

theorem preserving_inverse (μ : Measure X) (ν : Measure Y)
    (A : Set X) (B : Set Y) (hA : MeasurableSet A) (hB : MeasurableSet B)
    (hAc : μ Aᶜ=0) (hBc : ν Bᶜ=0) (e : A ≃ᵐ B)
    (he : MeasurePreserving e (μ.comap (Subtype.val : A → X))
      (ν.comap (Subtype.val : B → Y))) (x₀ : X) :
    MeasurePreserving (inverse A B e x₀) ν μ := by
…

Mentions: OAI.SmoothObstruction.ConullTransport.inverse

lemma OAI.SmoothObstruction.ConullTransport.invariant_iterates line 103

theorem OAI.SmoothObstruction.ConullTransport.inverse_iterates line 114

Source documentation

The total representative intertwines every nonnegative iterate on the original invariant conull set, not merely as unrelated a.e. identities.

theorem inverse_iterates (A : Set X) (B : Set Y) (e : A ≃ᵐ B) (x₀ : X)
    (T : X → X) (S : Y → Y) (hA : T ⁻¹' A=A) (hB : S ⁻¹' B=B)
    (heq : ∀ (x y : A),T x=y → (e y : Y)=S (e x)) :
    ∀ n,∀ y∈B,inverse A B e x₀ ((S^[n]) y)=(T^[n]) (inverse A B e x₀ y) := by
…

Mentions: OAI.SmoothObstruction.ConullTransport.inverse

theorem OAI.SmoothObstruction.ConullTransport.from_conjugate line 138

Source documentation

Faithful observation transport supplied by the literal conull conjugacy. In particular ALL finite name distributions can be pushed through r.

theorem from_conjugate (μ : Measure X) (ν : Measure Y) (T : X → X) (S : Y → Y)
    (h : SmoothObstruction.ConullConjugate μ T ν S) (x₀ : X) :
    ∃ r : Y → X,MeasurePreserving r ν μ ∧
      ∃ B : Set Y,MeasurableSet B ∧ ν Bᶜ=0 ∧ S ⁻¹' B=B ∧
        ∀ n,∀ y∈B,r ((S^[n]) y)=(T^[n]) (r y) := by
…

Mentions: OAI.SmoothObstruction.ConullConjugate

lemma OAI.SmoothObstruction.ConullTransport.invariant_inverse line 152
theorem OAI.SmoothObstruction.ConullTransport.inverse_time line 160
Source documentation
The same original invariant conull set supports both time directions. No countable collection of unrelated a.e. conjugacies is substituted.
```
theorem inverse_time (r : Y → X) (T : X ≃ X) (S : Y ≃ Y)
    (B : Set Y) (hB : S ⁻¹' B=B)
    (h : ∀ n,∀ y∈B,r ((S^[n]) y)=(T^[n]) (r y)) :
    ∀ n,∀ y∈B,r ((S.symm^[n]) y)=(T.symm^[n]) (r y) := by
…
```

theorem OAI.SmoothObstruction.ConullTransport.from_conjugate_bilateral line 183

Source documentation

Faithful bilateral observation transport from the literal main's conjugacy, including the invariant-conull and exact law clauses.

theorem from_conjugate_bilateral (μ : Measure X) (ν : Measure Y)
    (T : X ≃ X) (S : Y ≃ Y) (h : SmoothObstruction.ConullConjugate μ T ν S) (x₀ : X) :
    ∃ r : Y → X,MeasurePreserving r ν μ ∧
      ∃ B : Set Y,MeasurableSet B ∧ ν Bᶜ=0 ∧ S ⁻¹' B=B ∧ S.symm ⁻¹' B=B ∧
        (∀ n,∀ y∈B,r ((S^[n]) y)=(T^[n]) (r y)) ∧
        (∀ n,∀ y∈B,r ((S.symm^[n]) y)=(T.symm^[n]) (r y)) := by
…

Mentions: OAI.SmoothObstruction.ConullConjugate