English
If IsGalois K L, there exists σ ∈ B ≃ₐ[A] B such that map σ P = Q.
Русский
Если IsGalois K L, существует σ ∈ Aut_A(B) такой, что map σ P = Q.
LaTeX
$$$\\exists \\sigma : B \\simeq_{A} B,\\; \\mathrm{map} \\sigma\\; P = Q$$$
Lean4
/-- Generalization of Rayleigh's theorem on Beatty sequences. Let `r` be a real number greater
than 1, and `1/r + 1/s = 1`. Then `B⁺_r` and `B⁺'_s` partition the positive integers. -/
theorem beattySeq_symmDiff_beattySeq'_pos {r s : ℝ} (hrs : r.HolderConjugate s) :
{beattySeq r k | k > 0} ∆ {beattySeq' s k | k > 0} = {n | 0 < n} :=
by
apply Set.eq_of_subset_of_subset
· rintro j (⟨⟨k, hk, hjk⟩, -⟩ | ⟨⟨k, hk, hjk⟩, -⟩)
· rw [Set.mem_setOf_eq, ← hjk, beattySeq, Int.floor_pos]
exact one_le_mul_of_one_le_of_one_le (by norm_cast) hrs.lt.le
· rw [Set.mem_setOf_eq, ← hjk, beattySeq', sub_pos, Int.lt_ceil, Int.cast_one]
exact one_lt_mul_of_le_of_lt (by norm_cast) hrs.symm.lt
intro j (hj : 0 < j)
have hb₁ : ∀ s ≥ 0, j ∈ {beattySeq s k | k > 0} ↔ j ∈ {beattySeq s k | k} :=
by
intro _ hs
refine ⟨fun ⟨k, _, hk⟩ ↦ ⟨k, hk⟩, fun ⟨k, hk⟩ ↦ ⟨k, ?_, hk⟩⟩
rw [← hk, beattySeq, Int.floor_pos] at hj
exact_mod_cast pos_of_mul_pos_left (zero_lt_one.trans_le hj) hs
have hb₂ : ∀ s ≥ 0, j ∈ {beattySeq' s k | k > 0} ↔ j ∈ {beattySeq' s k | k} :=
by
intro _ hs
refine ⟨fun ⟨k, _, hk⟩ ↦ ⟨k, hk⟩, fun ⟨k, hk⟩ ↦ ⟨k, ?_, hk⟩⟩
rw [← hk, beattySeq', sub_pos, Int.lt_ceil, Int.cast_one] at hj
exact_mod_cast pos_of_mul_pos_left (zero_lt_one.trans hj) hs
rw [Set.mem_symmDiff, hb₁ _ hrs.nonneg, hb₂ _ hrs.symm.nonneg, ← compl_beattySeq hrs, Set.notMem_compl_iff,
Set.mem_compl_iff, and_self, and_self]
exact or_not
