Main.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SmoothObstruction.euclidean_switching line 16
theorem OAI.SmoothObstruction.halfspace_switching line 32
theorem OAI.SmoothObstruction.no_euclidean_model line 55
Source documentation
No closed smooth positive-density model in any finite dimension. The compatible metric used in the switching proof is chosen from the given topology; no metric or orientability hypothesis is imposed on the model.
```
theorem no_euclidean_model (μ : Measure Extension) [IsProbabilityMeasure μ]
    (hT : MeasurePreserving T μ μ) (d : ℕ) :
    ¬ HasModelWith μ T (𝓡 d) := by
…
```
Mentions: OAI.SmoothObstruction.HasModelWith
theorem OAI.SmoothObstruction.no_halfspace_model line 81
Source documentation
The same obstruction for smooth boundary manifolds, with their genuine half-space chart densities. No orientability assumption is introduced.
```
theorem no_halfspace_model (μ : Measure Extension) [IsProbabilityMeasure μ]
    (hT : MeasurePreserving T μ μ) (d : ℕ) [NeZero d] :
    ¬ HasModelWith μ T (𝓡∂ d) := by
…
```
Mentions: OAI.SmoothObstruction.HasModelWith
lemma OAI.SmoothObstruction.measurable_word_inverse line 107
Source documentation
Both sides of the phase-extension shift have the original product sigma-algebra measurability, independent of any choice of compatible metrics.
```
lemma measurable_word_inverse : Measurable (T.symm : Extension → Extension) := by
…
```
def OAI.SmoothObstruction.wordMeasurableEquiv line 116
theorem OAI.SmoothObstruction.main line 124
Source documentation
An ergodic invertible finite-KS-entropy transformation of a standard nonatomic probability space, with no compact finite-dimensional smooth strictly-positive-density model even modulo invariant null sets.
Distinct definitions of this name: ComparatorChallenges/SmoothObstruction.lean:90 (same statement text; different proof or body). Qualify references as OAI.SmoothObstruction.main@path.
```
theorem main :
    ∃ (X : Type) (_ : MeasurableSpace X) (μ : Measure X)
      (_ : IsProbabilityMeasure μ) (T : X ≃ᵐ X),
      StandardNonatomic μ ∧ Ergodic T μ ∧ FiniteKSEntropy μ T ∧
        ¬ HasSmoothPositiveVolumeModel μ T := by
…
```
Mentions: OAI.SmoothObstruction.StandardNonatomic, OAI.SmoothObstruction.FiniteKSEntropy, OAI.SmoothObstruction.HasSmoothPositiveVolumeModel