repr_opow_aux₂ — Mathlib

English

For a0,a' in ONote with NF, and for m ∈ Nat, d : ω ∣ repr a', e0 : repr a0 ≠ 0, and h describing a' + m < ω^{repr a0}, then a detailed equality holds between several structured components R and powers of ω^{repr a0}. This expresses a recursive decomposition of opowAux terms at a higher level of the ordinal hierarchy.

Русский

Для a0, a' в ONote с NF и для m ∈ Nat, d : ω ∣ repr a', e0 : repr a0 ≠ 0, и h описывающий a' + m < ω^{repr a0}, выполняется детальное равенство между несколькими структурированными компонентами R и степенями ω^{repr a0}. Это выражает рекурсивную декомпозицию элементов opowAux на более высоком уровне иерархии ординалов.

LaTeX

$$$\\forall (a_0\\,a')\\,[N0:\\ NF\\ a_0][Na': NF\\ a']\\; (m:\\ Nat)\\ (d : ω \\mid \\operatorname{repr} a')\\ (e0 : \\operatorname{repr} a_0 \\neq 0)\\ (h : \\operatorname{repr} a' + m < (ω^{\\operatorname{repr} a_0}))\\ (n : \\mathbb{N}) (k : \\mathbb{N}) :\\lobang\n \\text{let } R := \\operatorname{repr}(\\operatorname{opowAux}(0,a_0,(oadd\\ a_0\\ n\\ a')\\, m)\\ k\\ m)\\n (k \\neq 0 \\rightarrow R < ((ω^{\\operatorname{repr} a_0})^{\\operatorname{succ}(k)})) \\land \\\\\n ((ω^{\\operatorname{repr} a_0})^{(k)}) * ((ω^{\\operatorname{repr} a_0}) * (n\\,):\\Nat + \\operatorname{repr} a') + R = ((ω^{\\operatorname{repr} a_0}) * (n) + \\operatorname{repr} a' + m)^{(succ\\ (k))}$$$

Lean4

theorem repr_opow_aux₂ {a0 a'} [N0 : NF a0] [Na' : NF a'] (m : ℕ) (d : ω ∣ repr a') (e0 : repr a0 ≠ 0)
    (h : repr a' + m < (ω ^ repr a0)) (n : ℕ+) (k : ℕ) :
    let R := repr (opowAux 0 a0 (oadd a0 n a' * ofNat m) k m)
    (k ≠ 0 → R < ((ω ^ repr a0) ^ succ (k : Ordinal))) ∧
      ((ω ^ repr a0) ^ (k : Ordinal)) * ((ω ^ repr a0) * (n : ℕ) + repr a') + R =
        ((ω ^ repr a0) * (n : ℕ) + repr a' + m) ^ succ (k : Ordinal) :=
  by
  intro R'
  haveI No : NF (oadd a0 n a') := N0.oadd n (Na'.below_of_lt' <| lt_of_le_of_lt (le_add_right _ _) h)
  induction k with
  | zero => cases m <;> simp [R', opowAux]
  | succ k IH =>
    -- rename R => R'

    let R := repr (opowAux 0 a0 (oadd a0 n a' * ofNat m) k m)
    let ω0 := ω ^ repr a0
    let α' := ω0 * n + repr a'
    change
      (k ≠ 0 → R < (ω0 ^ succ (k : Ordinal))) ∧ (ω0 ^ (k : Ordinal)) * α' + R = (α' + m) ^ (succ ↑k : Ordinal) at IH
    have RR : R' = ω0 ^ (k : Ordinal) * (α' * m) + R :=
      by
      by_cases h : m = 0
      · simp only [R, R', h, ONote.ofNat, Nat.cast_zero, ONote.repr, mul_zero, ONote.opowAux, add_zero]
      ·
        simp only [α', ω0, R, R', ONote.repr_scale, ONote.repr, ONote.mulNat_eq_mul, ONote.opowAux, ONote.repr_ofNat,
          ONote.repr_mul, ONote.repr_add, Ordinal.opow_mul, ONote.zero_add]
    have α0 : 0 < α' := by simpa [lt_def, repr] using oadd_pos a0 n a'
    have ω00 : 0 < ω0 ^ (k : Ordinal) := opow_pos _ (opow_pos _ omega0_pos)
    have Rl : R < ω ^ (repr a0 * succ ↑k) := by
      by_cases k0 : k = 0
      · simp only [k0, Nat.cast_zero, succ_zero, mul_one, R]
        refine lt_of_lt_of_le ?_ (opow_le_opow_right omega0_pos (one_le_iff_ne_zero.2 e0))
        rcases m with - | m <;> simp [opowAux, omega0_pos]
        rw [← add_one_eq_succ, ← Nat.cast_succ]
        apply nat_lt_omega0
      · rw [opow_mul]
        exact IH.1 k0
    refine ⟨fun _ => ?_, ?_⟩
    · rw [RR, ← opow_mul _ _ (succ k.succ)]
      have e0 := Ordinal.pos_iff_ne_zero.2 e0
      have rr0 : 0 < repr a0 + repr a0 := lt_of_lt_of_le e0 (le_add_left _ _)
      apply principal_add_omega0_opow
      · simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, add_one_eq_succ, opow_mul, opow_succ, mul_assoc]
        gcongr ?_ * ?_
        rw [← Ordinal.opow_add]
        have : _ < ω ^ (repr a0 + repr a0) := (No.below_of_lt ?_).repr_lt
        · exact mul_lt_omega0_opow rr0 this (nat_lt_omega0 _)
        · simpa using (add_lt_add_iff_left (repr a0)).2 e0
      ·
        exact
          lt_of_lt_of_le Rl
            (opow_le_opow_right omega0_pos <|
              mul_le_mul_left' (succ_le_succ_iff.2 (Nat.cast_le.2 (le_of_lt k.lt_succ_self))) _)
    calc
      (ω0 ^ (k.succ : Ordinal)) * α' + R'
      _ = (ω0 ^ succ (k : Ordinal)) * α' + ((ω0 ^ (k : Ordinal)) * α' * m + R) := by rw [natCast_succ, RR, ← mul_assoc]
      _ = ((ω0 ^ (k : Ordinal)) * α' + R) * α' + ((ω0 ^ (k : Ordinal)) * α' + R) * m := ?_
      _ = (α' + m) ^ succ (k.succ : Ordinal) := by rw [← mul_add, natCast_succ, opow_succ, IH.2]
    congr 1
    · have αd : ω ∣ α' := dvd_add (dvd_mul_of_dvd_left (by simpa using opow_dvd_opow ω (one_le_iff_ne_zero.2 e0)) _) d
      rw [mul_add (ω0 ^ (k : Ordinal)), add_assoc, ← mul_assoc, ← opow_succ,
        add_mul_of_isSuccLimit _ (isSuccLimit_iff_omega0_dvd.2 ⟨ne_of_gt α0, αd⟩), mul_assoc,
        @mul_omega0_dvd n (Nat.cast_pos'.2 n.pos) (nat_lt_omega0 _) _ αd]
      apply @add_absorp _ (repr a0 * succ ↑k)
      · refine principal_add_omega0_opow _ ?_ Rl
        rw [opow_mul, opow_succ]
        gcongr
        exact No.snd'.repr_lt
      · have := mul_le_mul_left' (one_le_iff_pos.2 <| Nat.cast_pos'.2 n.pos) (ω0 ^ succ (k : Ordinal))
        rw [opow_mul]
        simpa [-opow_succ]
    · cases m
      · have : R = 0 := by cases k <;> simp [R, opowAux]
        simp [this]
      · rw [natCast_succ, add_mul_succ]
        apply add_absorp Rl
        rw [opow_mul, opow_succ]
        apply mul_le_mul_left'
        simpa [repr] using omega0_le_oadd a0 n a'

Похожие утверждения