I hate floor

Changes

3 changed files (+107/-6)

• Floor.lean (new)
  • @@ -0,0 +1,59 @@
    + import Mathlib + + def check := Id.run do + for j in [1:99] do + for k in [1:49] do + let x := (100 : ℚ) / 99 * j + let y := (99 : ℚ) * k / 98 / j + let z := (98 : ℚ) / k + if x * y * z ≠ 100 ∨ x.floor * y * z ≠ 99 ∨ (x * y).floor * z ≠ 98 then + return false + return true + + example : check = true := by + native_decide + + example {x y z : ℚ} (hx : 0 ≤ x) (hy : 0 ≤ y) + (h₁ : x * y * z = 100) (h₂ : x.floor * y * z = 99) (h₃ : (x * y).floor * z = 98) : + ∃ j k, 0 < j ∧ j < 99 ∧ 0 < k ∧ k < 49 + ∧ x = (100 : ℚ) / 99 * j ∧ y = (99 : ℚ) * k / 98 / j ∧ z = (98 : ℚ) / k := by + use x.floor, (x * y).floor + and_intros + · by_contra! h + suffices x.floor = 0 by grind [this ▸ h₂] + norm_cast at h + have : Rat.floor 0 = 0 := rfl + linarith [this ▸ Rat.floor_monotone hx] + · have : 100 * x.floor < 99 * (x.floor + 1) := by + have : 100 * x.floor = 99 * x := by grind + have : 100 * x.floor < 99 * ((x.floor : ℚ) + 1) := by grind [Rat.lt_floor_add_one x] + norm_cast at this + norm_cast + grind + · by_contra! h + suffices (x * y).floor = 0 by grind [this ▸ h₃] + norm_cast at h + have hxy : 0 ≤ x * y := by positivity + have : Rat.floor 0 = 0 := rfl + linarith [this ▸ Rat.floor_monotone hxy] + · have : 50 * (x * y).floor < 49 * ((x * y).floor + 1) := by + have : 50 * (x * y).floor = 49 * x * y := by grind + have : 50 * (x * y).floor < 49 * (((x * y).floor : ℚ) + 1) := by grind [Rat.lt_floor_add_one <| x * y] + norm_cast at this + norm_cast + grind + all_goals grind + + /- + Bad proof: + + set_option maxHeartbeats 1000000 in + example {j k : ℕ} (hj : 0 < j ∧ j < 99) (hk : 0 < k ∧ k < 49) : + let x := (100 : ℚ) / 99 * j + let y := (99 : ℚ) * k / 98 / j + let z := (98 : ℚ) / k + x * y * z = 100 ∧ x.floor * y * z = 99 ∧ (x * y).floor * z = 98 := by + obtain ⟨_, _⟩ := hj + obtain ⟨_, _⟩ := hk + interval_cases j <;> interval_cases k <;> native_decide + -/
• Gcd.lean
  • @@ -2,8 +2,7 @@ def gcd (a b : Nat) : Nat :=
    if b > 0 then gcd b (a % b) else a termination_by b decreasing_by - rename_i h - exact Nat.mod_lt a h + exact Nat.mod_lt a (by assumption) def N := 1000
• Homepage.lean
  • @@ -1,12 +1,55 @@
    import Mathlib - open Nat Quaternion Real CoxeterMatrix Lean + open Nat Real Quaternion CoxeterMatrix Lean + + def perm_of_gen (n : ℕ) (i : Fin n) : Equiv.Perm (Fin (n + 1)) := + Equiv.swap (Fin.castSucc i) (Fin.succ i) + + def toPerm (n : ℕ) : CoxeterMatrix.Group (Aₙ n) →* Equiv.Perm (Fin (n + 1)) := + PresentedGroup.toGroup (f := perm_of_gen n) (by + unfold Aₙ relationsSet relation perm_of_gen + simp + intro r x y h + subst h + split_ifs + next h => + subst h + simp + next h => + simp + obtain h|h := h + · ext i + simp + rcases x with ⟨ _ | x, hx ⟩ <;> rcases y with ⟨ _ | x_1, hx_1 ⟩ <;> norm_num [Fin.ext_iff, pow_succ', Equiv.swap_apply_def] at * + · subst h + simp_all only [zero_add, reduceAdd] + rcases i with ⟨ _ | _ | _ | i, hi ⟩ <;> norm_num [pow_three, Equiv.swap_apply_def] + simp +arith +decide [Fin.ext_iff] + · grind + + + ) + + lemma toPerm_bij (n : ℕ) : Function.Bijective <| toPerm n := by + constructor + · intro a b h + -- rw [toPerm, PresentedGroup.toGroup] at h + + · intro a + + #eval (Aₙ 2).Group + + example : Nat.card (Aₙ 2).Group = 6 := by + unfold Aₙ CoxeterMatrix.Group relationsSet relation + simp + - set_option maxRecDepth 1000 lemma A2_weyl_group_card : Nat.card (Aₙ 2).Group = 6 := by - -- TODO - sorry + rw [card_eq_of_bijective (toPerm 2) (toPerm_bij 2), card_eq_fintype_card] + rfl + + set_option maxRecDepth 1000 example : minFac '⓫'.toNat|>λ_11↦(·+97)<$>[0/0,_11,-(⟨1,0,2,4⟩:ℍ[ℤ])^2|>.re.toNat,defaultMaxRecDepth%101,catalan 4,_11,(φ∘φ∘φ∘φ∘φ∘φ<|4‼‼)!,↑((4:Fin 24)-6),⌈deriv (sin ·^69) π⌉₊,_11,Nat.card<|Aₙ 2|>.Group] = "anthonywang".toList.map Char.toNat := by