Theory $\mathsf{I}{\mathrm{\Sigma }}_0+{\mathrm{\Omega }}_1$

def LO.Omega1.omega1 : FirstOrder.SyntacticFormula ℒₒᵣ

∀ x, ∃ y, 2^{|x|^2} = y

Equations

• One or more equations did not get rendered due to their size.

inductive LO.Omega1 : FirstOrder.Theory ℒₒᵣ

• omega : 𝛀₁ omega1

Instances For

• LO.Omega1.instModelsTheory

def LO.Omega1.«term𝛀₁» : Lean.ParserDescr

Equations

• LO.Omega1.«term𝛀₁» = Lean.ParserDescr.node `LO.Omega1.«term𝛀₁» 1024 (Lean.ParserDescr.symbol "𝛀₁")

@[simp]

theorem LO.FirstOrder.Theory.OmegaOne.mem_iff {σ : SyntacticFormula ℒₒᵣ} : σ ∈ 𝛀₁ ↔ σ = Omega1.omega1

theorem LO.Omega1.models_Omega1_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : V ⊧ₘ omega1 ↔ ∀ (x : V), ∃ (y : V), ISigma0.Exponential (‖x‖ ^ 2) y

theorem LO.Omega1.omega1_of_ISigma1 {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : V ⊧ₘ omega1

instance LO.Omega1.instModelsTheoryHAddTheoryORingISigmaOfNatNat {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁

instance LO.Omega1.instModelsTheoryISigmaOfNatNat {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : V ⊧ₘ* 𝐈𝚺₀

instance LO.Omega1.instModelsTheory {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : V ⊧ₘ* 𝛀₁

theorem LO.Omega1.exists_exponential_sq_length {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (x : V) : ∃ (y : V), ISigma0.Exponential (‖x‖ ^ 2) y

theorem LO.Omega1.exists_unique_exponential_sq_length {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (x : V) : ∃! y : V, ISigma0.Exponential (‖x‖ ^ 2) y

theorem LO.Omega1.smash_exists_unique {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (x y : V) : ∃! z : V, ISigma0.Exponential (‖x‖ * ‖y‖) z

instance LO.Omega1.instSmash {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : Smash V

Equations

• LO.Omega1.instSmash = { smash := fun (a b : V) => Classical.choose! ⋯ }

theorem LO.Omega1.exponential_smash {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a b : V) : ISigma0.Exponential (‖a‖ * ‖b‖) (a ⨳ b)

theorem LO.Omega1.exponential_smash_one {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) : ISigma0.Exponential ‖a‖ (a ⨳ 1)

def LO.Omega1.smashDef : 𝚺₀.Semisentence 3

Equations

• One or more equations did not get rendered due to their size.

theorem LO.Omega1.smash_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : 𝚺₀-Function₂ Smash.smash via smashDef

instance LO.Omega1.smash_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : 𝚺₀-Function₂ Smash.smash

@[simp]

theorem LO.Omega1.smash_pow2 {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a b : V) : ISigma0.Pow2 (a ⨳ b)

@[simp]

theorem LO.Omega1.smash_pos {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a b : V) : 0 < a ⨳ b

@[simp]

theorem LO.Omega1.smash_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a b : V) : ‖a‖ * ‖b‖ < a ⨳ b

theorem LO.Omega1.length_smash {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a b : V) : ‖a ⨳ b‖ = ‖a‖ * ‖b‖ + 1

@[simp]

theorem LO.Omega1.smash_zero_left {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) : 0 ⨳ a = 1

@[simp]

theorem LO.Omega1.smash_zero_right {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) : a ⨳ 0 = 1

theorem LO.Omega1.smash_comm {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a b : V) : a ⨳ b = b ⨳ a

@[simp]

theorem LO.Omega1.lt_smash_one_right {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) : a < a ⨳ 1

@[simp]

theorem LO.Omega1.lt_smash_one_righs {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) : a ⨳ 1 ≤ 2 * a + 1

theorem LO.Omega1.lt_smash_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {a b c : V} : a < b ⨳ c ↔ ‖a‖ ≤ ‖b‖ * ‖c‖

theorem LO.Omega1.smash_le_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {a b c : V} : b ⨳ c ≤ a ↔ ‖b‖ * ‖c‖ < ‖a‖

theorem LO.Omega1.lt_smash_one_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {a b : V} : a < b ⨳ 1 ↔ ‖a‖ ≤ ‖b‖

theorem LO.Omega1.smash_monotone {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {a₁ a₂ b₁ b₂ : V} (h₁ : a₁ ≤ b₁) (h₂ : a₂ ≤ b₂) : a₁ ⨳ a₂ ≤ b₁ ⨳ b₂

theorem LO.Omega1.bexp_eq_smash {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a b : V) : ISigma0.bexp (a ⨳ b) (‖a‖ * ‖b‖) = a ⨳ b

theorem LO.Omega1.smash_two_mul {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) {b : V} (pos : 0 < b) : a ⨳ (2 * b) = a ⨳ b * a ⨳ 1

theorem LO.Omega1.smash_two_mul_le_sq_smash {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a b : V) : a ⨳ (2 * b) ≤ (a ⨳ b) ^ 2

instance LO.Omega1.instWeakerThanSyntacticFormulaORingTheoryISigmaOfNatNatHAdd : 𝐈𝚺₀ ⪯ 𝐈𝚺₀ + 𝛀₁

instance LO.Omega1.instWeakerThanSyntacticFormulaORingTheoryHAddISigmaOfNatNat : 𝐈𝚺₀ + 𝛀₁ ⪯ 𝐈𝚺₁

instance LO.Omega1.instModelsTheoryNatHAddTheoryORingISigmaOfNat : ℕ ⊧ₘ* 𝐈𝚺₀ + 𝛀₁