More sloppppppppp

Changes

3 changed files (+870/-0)

• CoxeterAristotle2.lean (new)
  • @@ -0,0 +1,574 @@
    + /- + Sorry, Aristotle was unable to complete the task in time. + -/ + /- + This file was generated by Aristotle. + + Lean version: leanprover/lean4:v4.24.0 + Mathlib version: f897ebcf72cd16f89ab4577d0c826cd14afaafc7 + -/ + + import Mathlib + + open scoped BigOperators + open scoped Real + open scoped Nat + open scoped Classical + open scoped Pointwise + + set_option maxHeartbeats 0 + set_option maxRecDepth 4000 + set_option synthInstance.maxHeartbeats 20000 + set_option synthInstance.maxSize 128 + + set_option relaxedAutoImplicit false + set_option autoImplicit false + + noncomputable section + + /- + The Weyl group of type A_n is the Coxeter group associated with the Coxeter matrix A_n. + -/ + open CoxeterMatrix + + def WeylGroupA (n : ℕ) := CoxeterMatrix.Group (Aₙ n) + + + /- + Checking definitions and instances. + -/ + open CoxeterMatrix + + #check CoxeterMatrix.Group + #check PresentedGroup.toGroup + #synth Group (CoxeterMatrix.Group (Aₙ 3)) + + /- + There is a homomorphism from the Weyl group of type A_n to the symmetric group S_{n+1}. + -/ + open CoxeterMatrix + + 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 CoxeterMatrix.Aₙ; + simp ( config := { decide := Bool.true } ) [ CoxeterMatrix.relationsSet ]; + unfold CoxeterMatrix.relation; aesop; + · ext i ; unfold perm_of_gen ; aesop; + · ext i; + unfold perm_of_gen; + rcases x with ⟨ _ | x, hx ⟩ <;> rcases x_1 with ⟨ _ | x_1, hx_1 ⟩ <;> norm_num [ Fin.ext_iff, pow_succ', Equiv.swap_apply_def ] at *; + · aesop; + rcases i with ⟨ _ | _ | _ | i, hi ⟩ <;> norm_num [ pow_three, Equiv.swap_apply_def ]; + simp +arith +decide [ Fin.ext_iff ]; + · grind; + · ext y ; simp ( config := { decide := Bool.true } ) [ *, perm_of_gen ]; + rcases x with ⟨ _ | x, hx ⟩ <;> rcases x_1 with ⟨ _ | x_1, hx_1 ⟩ <;> norm_num [ Fin.ext_iff, Equiv.swap_apply_def ] at *; + · aesop; + rcases y with ⟨ _ | _ | _ | y, hy ⟩ <;> norm_num [ pow_succ, Equiv.swap_apply_def ]; + simp ( config := { decide := Bool.true } ) [ Fin.ext_iff, Nat.succ_eq_add_one ] at *; + · -- By definition of permutation multiplication, we can see that applying the permutation three times returns each element to its original position. + simp [Equiv.swap_apply_def, pow_succ']; + grind; + · -- Since $x \neq x_1$, the permutations $perm_of_gen n x$ and $perm_of_gen n x_1$ commute. + have h_comm : perm_of_gen n x * perm_of_gen n x_1 = perm_of_gen n x_1 * perm_of_gen n x := by + ext y; simp [perm_of_gen]; + by_cases hy : y = x.castSucc <;> by_cases hy' : y = x.succ <;> by_cases hy'' : y = x_1.castSucc <;> by_cases hy''' : y = x_1.succ <;> simp_all +decide [ Equiv.swap_apply_def ]; + all_goals simp_all ( config := { decide := Bool.true } ) [ Fin.ext_iff, Fin.val_add ]; + · aesop; + · aesop; + simp_all +decide [ pow_succ, mul_assoc ]; + simp_all +decide [ ← mul_assoc ]; + simp_all +decide [ mul_assoc, perm_of_gen ]) + + /- + The homomorphism `toPerm` from the Weyl group of type A_n to the symmetric group S_{n+1} is surjective. + -/ + theorem toPerm_surjective (n : ℕ) : Function.Surjective (toPerm n) := by + -- To prove surjectivity, it suffices to show that the image of `toPerm` contains all the adjacent transpositions, which generate the symmetric group. + have h_adj_transpositions : ∀ i : Fin n, ∃ g : CoxeterMatrix.Group (Aₙ n), toPerm n g = Equiv.swap (Fin.castSucc i) (Fin.succ i) := by + intro i; + exact ⟨ PresentedGroup.of i, by aesop ⟩; + -- Since the symmetric group is generated by the adjacent transpositions, and we have shown that the image of `toPerm` contains all these transpositions, the image must be the entire symmetric group. + have h_image : ∀ p : Equiv.Perm (Fin (n + 1)), ∃ g : CoxeterMatrix.Group (Aₙ n), toPerm n g = p := by + intro p + have h_gen : p ∈ Subgroup.closure (Set.range (fun i : Fin n => Equiv.swap (Fin.castSucc i) (Fin.succ i))) := by + -- The symmetric group $S_{n+1}$ is generated by the adjacent transpositions $(i, i+1)$ for $i \in \{0, 1, \ldots, n-1\}$. + have h_gen : ∀ p : Equiv.Perm (Fin (n + 1)), p ∈ Subgroup.closure (Set.range (fun i : Fin n => Equiv.swap (Fin.castSucc i) (Fin.succ i))) := by + intro p + have h_adj_transpositions : ∀ i : Fin (n + 1), ∀ j : Fin (n + 1), i < j → Equiv.swap i j ∈ Subgroup.closure (Set.range (fun i : Fin n => Equiv.swap (Fin.castSucc i) (Fin.succ i))) := by + intro i j hij; induction' j using Fin.inductionOn with j ih ih; aesop; + cases lt_or_eq_of_le ( show i ≤ Fin.castSucc j from Nat.le_of_lt_succ hij ) <;> simp_all +decide [ Subgroup.mem_closure ]; + · intro K hK; specialize ih K hK; specialize hK ( Set.mem_range_self j ) ; aesop; + exact?; + · exact fun K hK => hK ⟨ j, rfl ⟩ + induction' p using Equiv.Perm.swap_induction_on' with p i j hij ih; + · exact OneMemClass.one_mem _; + · exact Subgroup.mul_mem _ ih ( if hij' : i < j then h_adj_transpositions i j hij' else by simpa only [ Equiv.swap_comm ] using h_adj_transpositions j i ( lt_of_le_of_ne ( le_of_not_gt hij' ) hij.symm ) ); + exact h_gen p + refine' Subgroup.closure_induction ( fun x hx => _ ) _ _ _ h_gen; + · aesop; + · exact ⟨ 1, map_one _ ⟩; + · rintro x y hx hy ⟨ g, rfl ⟩ ⟨ h, rfl ⟩ ; exact ⟨ g * h, by simp +decide ⟩ ; + · rintro x hx ⟨ g, rfl ⟩ ; exact ⟨ g⁻¹, by simp +decide ⟩ ; + exact h_image + + /- + We define the index set for the roots of type A_n as the set of pairs of distinct indices from 0 to n. We prove it is a finite type. + -/ + variable (n : ℕ) + + def TypeA.ι := { x : Fin (n + 1) × Fin (n + 1) // x.1 ≠ x.2 } + + instance : Fintype (TypeA.ι n) := + have : DecidablePred (fun x : Fin (n + 1) × Fin (n + 1) => x.1 ≠ x.2) := fun _ => inferInstance + inferInstanceAs (Fintype { x : Fin (n + 1) × Fin (n + 1) // x.1 ≠ x.2 }) + + instance : DecidableEq (TypeA.ι n) := inferInstance + + /- + We define the index set for the roots of type A_n as the set of pairs of distinct indices from 0 to n. We prove it is a finite type. + -/ + variable (n : ℕ) + + abbrev TypeA_Indices := { x : Fin (n + 1) × Fin (n + 1) // x.1 ≠ x.2 } + + instance : Fintype (TypeA_Indices n) := inferInstance + instance : DecidableEq (TypeA_Indices n) := inferInstance + + /- + We define the roots and coroots for the root system of type A. For each index pair (i, j), the root and coroot are both the vector e_i - e_j in Z^{n+1}. + -/ + variable (n : ℕ) + + def TypeA.root (i : TypeA_Indices n) : Fin (n + 1) → ℤ := + Pi.single i.1.1 1 - Pi.single i.1.2 1 + + def TypeA.coroot (i : TypeA_Indices n) : Fin (n + 1) → ℤ := + Pi.single i.1.1 1 - Pi.single i.1.2 1 + + /- + Checking the type of Matrix.toBilin. + -/ + #check Matrix.toBilin + + /- + We define the perfect pairing for the root system of type A as the standard dot product. We also define the reflection permutation associated with a root index (i, j) as the permutation of indices induced by the transposition (i, j). + -/ + variable (n : ℕ) + + def TypeA.pairing : PerfectPairing ℤ (Fin (n + 1) → ℤ) (Fin (n + 1) → ℤ) := + { toLinearMap := LinearMap.mk₂ ℤ dotProduct (by + -- The dot product is linear in the first argument, so we can split the sum into two parts. + intros m₁ m₂ n + simp [dotProduct, add_mul, Finset.sum_add_distrib]) (by + -- The dot product is linear in both arguments, so we can distribute the scalar multiplication over the dot product. + intros c m n + simp [dotProduct, mul_assoc, mul_comm, mul_left_comm]; + -- Apply the distributive property of multiplication over addition. + rw [Finset.mul_sum]) (by + -- By the distributive property of multiplication over addition, we can split the sum into two separate sums. + intros m n₁ n₂ + simp [mul_add, Finset.sum_add_distrib]) (by + -- The dot product is linear, so we can distribute the scalar multiplication over the dot product. + intros c m n_1 + simp [dotProduct, smul_eq_mul]; + -- By the properties of multiplication, we can factor out the scalar $c$ from the sum. + simp [mul_assoc, mul_comm, mul_left_comm, Finset.mul_sum]) + bijective_left := by + constructor; + · intro m m' h; ext i; replace h := congr_arg ( fun f => f ( Pi.single i 1 ) ) h; aesop; + · -- To show surjectivity, take any linear functional $f$ on $\mathbb{Z}^{n+1}$. We can represent $f$ as the dot product with some vector $v$. + intro f + use fun i => f (Pi.single i 1); + bound + bijective_right := by + constructor <;> intro f <;> aesop + generalize_proofs at *; + ext i; have := congr_arg ( fun f => f ( Pi.single i 1 ) ) a; norm_num at this; aesop; } + + def TypeA.reflectionPerm (i : TypeA_Indices n) : Equiv.Perm (TypeA_Indices n) := + let σ := Equiv.swap i.1.1 i.1.2 + { toFun := fun x => ⟨(σ x.1.1, σ x.1.2), by + intro h + apply x.2 + apply σ.injective + exact h⟩ + invFun := fun x => ⟨(σ x.1.1, σ x.1.2), by + intro h + apply x.2 + apply σ.injective + exact h⟩ + left_inv := by intro x; simp; apply Subtype.ext; simp; rw [Equiv.swap_apply_self, Equiv.swap_apply_self] + right_inv := by intro x; simp; apply Subtype.ext; simp; rw [Equiv.swap_apply_self, Equiv.swap_apply_self] } + + /- + Checking the definition of RootPairing. + -/ + #print RootPairing + + /- + Checking if TypeA.pairing and TypeA.reflectionPerm are already defined. + -/ + variable (n : ℕ) + + #check TypeA.pairing + #check TypeA.reflectionPerm + + /- + We define the embedding of the roots of type A into the ambient space. The injectivity proof is left as a sorry. + -/ + variable (n : ℕ) + + def TypeA.rootEmbedding : TypeA_Indices n ↪ (Fin (n + 1) → ℤ) := + Function.Embedding.mk (TypeA.root n) (by + intro x y hxy; + unfold TypeA.root at hxy; + replace hxy := congr_fun hxy; + have := hxy x.1.1; have := hxy x.1.2; have := hxy y.1.1; have := hxy y.1.2; simp_all +decide [ Fin.ext_iff, Pi.single_apply ] ; + grind +ring) + + /- + We define the embedding of the coroots of type A into the ambient space. The injectivity proof is identical to that of the roots. + -/ + variable (n : ℕ) + + def TypeA.corootEmbedding : TypeA_Indices n ↪ (Fin (n + 1) → ℤ) := + Function.Embedding.mk (TypeA.coroot n) (by + intro x y hxy; + unfold TypeA.coroot at hxy; + replace hxy := congr_fun hxy; + have := hxy x.1.1; have := hxy x.1.2; have := hxy y.1.1; have := hxy y.1.2; simp_all +decide [ Fin.ext_iff, Pi.single_apply ] ; + grind +ring) + + /- + The map `TypeA.root` is injective. + -/ + variable (n : ℕ) + + lemma TypeA.root_injective : Function.Injective (TypeA.root n) := by + intro i j h + unfold TypeA.root at h + -- We have e_i - e_j = e_k - e_l + -- This implies {i, l} = {k, j} as multisets if we look at the support, + -- but since i != j and k != l, we can deduce i = k and j = l. + -- We can use function extensionality to look at specific coordinates. + have h_i := congr_fun h i.1.1 + have h_j := congr_fun h i.1.2 + simp [Pi.single_apply] at h_i h_j + -- We need to handle cases where indices might coincide. + -- Since i.1.1 != i.1.2, we know the value at i.1.1 is 1 and at i.1.2 is -1. + -- The RHS must match this. + grind + + /- + We define the root pairing for type A_n. We register the perfect pairing instance and then construct the `RootPairing` structure using the embeddings and permutations defined earlier. We leave the verification of the axioms as sorries. + -/ + variable (n : ℕ) + + instance : LinearMap.IsPerfPair (TypeA.pairing n).toLinearMap := + { bijective_left := (TypeA.pairing n).bijective_left + bijective_right := (TypeA.pairing n).bijective_right } + + def RootPairingA : RootPairing (TypeA_Indices n) ℤ (Fin (n + 1) → ℤ) (Fin (n + 1) → ℤ) where + toLinearMap := (TypeA.pairing n).toLinearMap + root := TypeA.rootEmbedding n + coroot := TypeA.corootEmbedding n + root_coroot_two := by + unfold TypeA.rootEmbedding TypeA.corootEmbedding; + unfold TypeA.pairing; + unfold TypeA.root TypeA.coroot; aesop + reflectionPerm := TypeA.reflectionPerm n + reflectionPerm_root := by + unfold TypeA.rootEmbedding TypeA.corootEmbedding TypeA.reflectionPerm; + -- By definition of reflection permutation, we have that the reflection of j under i is equal to the permutation of j under the swap of i's components. + simp [TypeA.root, TypeA.coroot, Equiv.swap_apply_def]; + intro a b hab a' b' hab'; ext i; aesop; + unfold TypeA.pairing; simp +decide [ Pi.single_apply ] ; + grind +ring + reflectionPerm_coroot := by + bound; + unfold TypeA.corootEmbedding TypeA.rootEmbedding TypeA.pairing TypeA.reflectionPerm; + -- By definition of reflection permutation, we have σ(j.1) = snd and σ(j.2) = fst if j.1 = fst and j.2 = snd, and vice versa. + simp [Equiv.swap_apply_def]; + unfold TypeA.root TypeA.coroot; aesop; + · ext; simp ( config := { decide := Bool.true } ) [ two_mul, sub_eq_add_neg ] ; ring; + · ext; norm_num; ring + + /- + We define the root pairing for type A_n. We register the perfect pairing instance and then construct the `RootPairing` structure using the embeddings and permutations defined earlier. We leave the verification of the axioms as sorries. + -/ + variable (n : ℕ) + + def RootPairingTypeA : RootPairing (TypeA_Indices n) ℤ (Fin (n + 1) → ℤ) (Fin (n + 1) → ℤ) where + toLinearMap := (TypeA.pairing n).toLinearMap + root := TypeA.rootEmbedding n + coroot := TypeA.corootEmbedding n + root_coroot_two := by + intro i + unfold TypeA.rootEmbedding TypeA.corootEmbedding TypeA.pairing TypeA.root TypeA.coroot + simp only [Function.Embedding.coeFn_mk] + -- We need to evaluate the pairing of (e_i - e_j) with itself. + -- The pairing is the dot product. + -- (e_i - e_j) . (e_i - e_j) = e_i.e_i - e_i.e_j - e_j.e_i + e_j.e_j + -- Since i != j, e_i.e_j = 0. + -- e_i.e_i = 1, e_j.e_j = 1. + -- So 1 - 0 - 0 + 1 = 2. + aesop + reflectionPerm := TypeA.reflectionPerm n + reflectionPerm_root := by + -- By definition of reflection, we know that $s_i(j) = j - \langle j, i^\vee \rangle i$. + intros i j + simp [TypeA.reflectionPerm, TypeA.rootEmbedding, TypeA.corootEmbedding]; + unfold TypeA.pairing TypeA.root TypeA.coroot; aesop; + simp ( config := { decide := Bool.true } ) [ Pi.single_apply, Equiv.swap_apply_def ]; + grind +ring + reflectionPerm_coroot := by + -- By definition of reflection permutation, we have that the reflection of j by i is the swap of the indices. + simp [TypeA.reflectionPerm]; + intro a b hab a' b' hab'; ext x; simp +decide [ Equiv.swap_apply_def ] ; + unfold TypeA.corootEmbedding TypeA.rootEmbedding; simp +decide [ TypeA.pairing ] ; + simp +decide [ TypeA.coroot, TypeA.root, dotProduct ]; + simp +decide [ Finset.sum_add_distrib, sub_mul, mul_sub, Pi.single_apply ]; + grind +ring + + /- + The reflection corresponding to the root indexed by `i` acts on the basis vector `e_k` by swapping indices according to the transposition `(i.1, i.2)`. + -/ + variable (n : ℕ) + + def WeylGroupTypeA := (RootPairingTypeA n).weylGroup + + lemma reflection_apply_basis (i : TypeA_Indices n) (k : Fin (n + 1)) : + (RootPairingTypeA n).reflection i (Pi.single k 1) = Pi.single (Equiv.swap i.1.1 i.1.2 k) 1 := by + unfold RootPairingTypeA; + -- By definition of reflection, we have that the reflection of the root i on the basis vector e_k is equal to the basis vector e_{σ(k)}, where σ is the transposition (i.1, i.2). + simp [RootPairing.reflection, TypeA.reflectionPerm]; + simp +decide [ Module.reflection ]; + unfold Module.preReflection TypeA.pairing TypeA.corootEmbedding TypeA.rootEmbedding; aesop; + unfold TypeA.coroot TypeA.root; aesop; + by_cases hk : k = fst <;> by_cases hk' : k = snd <;> simp +decide [ *, Pi.single_apply ]; + rw [ Equiv.swap_apply_of_ne_of_ne hk hk' ] + + /- + Checking the definition of RootPairing.Equiv. + -/ + #print RootPairing.Equiv + + /- + For every element `w` in the Weyl group of type A, there exists a permutation `σ` of the indices such that `w` acts on the basis vectors by permuting them according to `σ`. + -/ + variable (n : ℕ) + + lemma basis_perm_exists (w : WeylGroupTypeA n) : + ∃ σ : Equiv.Perm (Fin (n + 1)), ∀ k, (w.val.weightMap : (Fin (n + 1) → ℤ) →ₗ[ℤ] (Fin (n + 1) → ℤ)) (Pi.single k 1) = Pi.single (σ k) 1 := by + -- By definition of the Weyl group, each element w corresponds to a permutation of the indices. + have h_perm : ∀ w : WeylGroupTypeA n, ∃ σ : Equiv.Perm (Fin (n + 1)), ∀ k : Fin (n + 1), (w.val.weightMap (Pi.single k 1)) = Pi.single (σ k) 1 := by + intro w + have h_gen : ∀ i : TypeA_Indices n, ∃ σ : Equiv.Perm (Fin (n + 1)), ∀ k : Fin (n + 1), (RootPairingTypeA n).reflection i (Pi.single k 1) = Pi.single (σ k) 1 := by + -- By definition of reflectionPerm, we know that it swaps the indices i.1.1 and i.1.2. + intro i + use Equiv.swap i.1.1 i.1.2; + -- By definition of reflection, we know that it swaps the indices i.1.1 and i.1.2. Therefore, for any k, the reflection of e_k is equal to the single vector at the swapped position. + intros k + apply reflection_apply_basis + induction' w with w hw; + induction hw using Subgroup.closure_induction; + · aesop; + · exact ⟨ Equiv.refl _, fun k => rfl ⟩; + · rename_i hx hy; + obtain ⟨ σ, hσ ⟩ := hx; obtain ⟨ τ, hτ ⟩ := hy; use σ * τ; intro k; simp +decide [ hσ, hτ ] ; + · rename_i hx; + obtain ⟨ σ, hσ ⟩ := hx; + use σ⁻¹; + -- By definition of the inverse automorphism, we have that $x⁻¹.weightMap (Pi.single (σ k) 1) = Pi.single k 1$. + have h_inv : ∀ k : Fin (n + 1), (‹(RootPairingTypeA n).Aut›⁻¹).weightMap (Pi.single (σ k) 1) = Pi.single k 1 := by + intro k; + rw [ ← hσ k ]; + convert LinearEquiv.symm_apply_apply _ _; + intro k; specialize h_inv ( σ⁻¹ k ) ; aesop; + exact h_perm w + + /- + For every element `w` in the Weyl group of type A, there exists a permutation `σ` of the indices such that `w` acts on the basis vectors by permuting them according to `σ`. + -/ + variable (n : ℕ) + + lemma weyl_group_acts_as_perm (w : WeylGroupTypeA n) : + ∃ σ : Equiv.Perm (Fin (n + 1)), ∀ k, w.val.weightMap (Pi.single k 1) = Pi.single (σ k) 1 := by + exact? + + /- + Checking the type of Pi.single_injective. + -/ + #check Pi.single_injective + + /- + We define the map from the Weyl group to the symmetric group by extracting the permutation that acts on the basis vectors. + -/ + variable (n : ℕ) + + def weylToPerm (w : WeylGroupTypeA n) : Equiv.Perm (Fin (n + 1)) := + Classical.choose (basis_perm_exists n w) + + lemma weylToPerm_apply (w : WeylGroupTypeA n) (k : Fin (n + 1)) : + (w.val.weightMap : (Fin (n + 1) → ℤ) →ₗ[ℤ] (Fin (n + 1) → ℤ)) (Pi.single k 1) = Pi.single (weylToPerm n w k) 1 := + Classical.choose_spec (basis_perm_exists n w) k + + /- + We define the group homomorphism from the Weyl group to the symmetric group. + -/ + variable (n : ℕ) + + def weylToPermHom : WeylGroupTypeA n →* Equiv.Perm (Fin (n + 1)) where + toFun := weylToPerm n + map_one' := by + have h_id : (1 : WeylGroupTypeA n).val.weightMap (Pi.single 0 1) = Pi.single (weylToPerm n 1 0) 1 := by + exact?; + ext i; replace h_id := congr_fun h_id i; aesop; + have := Classical.choose_spec ( basis_perm_exists n ( w := 1 ) ) i; aesop; + replace this := congr_fun this ( ( Classical.choose ( basis_perm_exists n ( w := 1 ) ) ) i ) ; aesop; + rw [ Pi.single_apply ] at this ; aesop; + exact congr_arg Fin.val this + map_mul' := by + -- By definition of weylToPerm, we have that for any x and y in the Weyl group, weylToPerm n (x * y) is the permutation that acts on the basis vectors by first applying y and then x. + intros x y + apply Equiv.Perm.ext + intro k + simp [weylToPerm_apply]; + have h_comp : ∀ (x y : WeylGroupTypeA n), (x * y).val.weightMap (Pi.single k 1) = (x.val.weightMap) ((y.val.weightMap) (Pi.single k 1)) := by + exact?; + have h_comp : (weylToPerm n (x * y)) k = (weylToPerm n x) ((weylToPerm n y) k) := by + have := h_comp x y + rw [ weylToPerm_apply, weylToPerm_apply, weylToPerm_apply ] at * ; aesop; + replace this := congr_fun this ( ( weylToPerm n ⟨ val, property ⟩ ) ( ( weylToPerm n ⟨ val_1, property_1 ⟩ ) k ) ) ; aesop; + rw [ Pi.single_apply ] at this ; aesop; + exact h_comp + + /- + The homomorphism from the Weyl group of type A to the symmetric group is bijective. + -/ + variable (n : ℕ) + + theorem weylToPermHom_bijective : Function.Bijective (weylToPermHom n) := by + -- To show surjectivity, notice that every permutation can be written as a product of simple reflections, which are in the image of the homomorphism. + have h_surjective : Function.Surjective (weylToPermHom n) := by + intro σ; + -- Let's choose any permutation σ of the indices. + obtain ⟨w, hw⟩ : ∃ w : WeylGroupTypeA n, ∀ k : Fin (n + 1), (w.val.weightMap : (Fin (n + 1) → ℤ) →ₗ[ℤ] (Fin (n + 1) → ℤ)) (Pi.single k 1) = Pi.single (σ k) 1 := by + -- Since the Weyl group is generated by the simple reflections, any permutation σ can be written as a product of these transpositions. + have h_gen : ∀ σ : Equiv.Perm (Fin (n + 1)), ∃ w : WeylGroupTypeA n, ∀ k : Fin (n + 1), (w.val.weightMap : (Fin (n + 1) → ℤ) →ₗ[ℤ] (Fin (n + 1) → ℤ)) (Pi.single k 1) = Pi.single (σ k) 1 := by + intro σ; + induction' σ using Equiv.Perm.swap_induction_on with σ a b hab hσ; + · refine' ⟨ ⟨ 1, _ ⟩, _ ⟩ <;> aesop; + · obtain ⟨ w, hw ⟩ := hσ; + -- Let $w'$ be the reflection corresponding to the transposition $(a, b)$. + obtain ⟨w', hw'⟩ : ∃ w' : WeylGroupTypeA n, ∀ k : Fin (n + 1), (w'.val.weightMap : (Fin (n + 1) → ℤ) →ₗ[ℤ] (Fin (n + 1) → ℤ)) (Pi.single k 1) = Pi.single (Equiv.swap a b k) 1 := by + have h_reflection : ∀ i : TypeA_Indices n, ∃ w' : WeylGroupTypeA n, ∀ k : Fin (n + 1), (w'.val.weightMap : (Fin (n + 1) → ℤ) →ₗ[ℤ] (Fin (n + 1) → ℤ)) (Pi.single k 1) = Pi.single (Equiv.swap i.1.1 i.1.2 k) 1 := by + bound; + exact ⟨ ⟨ _, Subgroup.subset_closure <| Set.mem_range_self ⟨ ⟨ fst, snd ⟩, property_1 ⟩ ⟩, reflection_apply_basis _ _ ⟩; + exact h_reflection ⟨ ( a, b ), hab ⟩; + use w' * w; + aesop; + exact h_gen σ; + use w; + -- Since the permutation is determined by its action on the basis vectors, and we have shown that w and σ act the same on all basis vectors, they must be the same permutation. + have h_perm_eq : ∀ k : Fin (n + 1), (weylToPerm n w) k = σ k := by + intro k; specialize hw k; replace hw := congr_fun hw ( σ k ) ; aesop; + have := weylToPerm_apply n ⟨ val, property ⟩ k; aesop; + rw [ Pi.single_apply ] at hw ; aesop; + exact Equiv.Perm.ext h_perm_eq; + -- To show injectivity, we need to show that the kernel of the homomorphism is trivial. + have h_kernel_trivial : ∀ w : WeylGroupTypeA n, weylToPermHom n w = 1 → w = 1 := by + bound; + -- If the permutation induced by the Weyl group element is the identity, then the Weyl group element itself must be the identity. + have h_id : ∀ k : Fin (n + 1), val.weightMap (Pi.single k 1) = Pi.single k 1 := by + intro k; have := Classical.choose_spec ( basis_perm_exists n ⟨ val, property ⟩ ) k; aesop; + replace a := congr_arg ( fun f => f k ) a ; aesop; + congr; + -- Since the weight map of the Weyl group element is the identity, the Weyl group element itself must be the identity. + have h_val_id : val.weightMap = LinearMap.id := by + aesop; + cases val ; aesop; + cases toHom ; aesop; + congr; + · ext x; + replace weight_coweight_transpose := congr_arg ( fun f => f ( Pi.single x 1 ) ) weight_coweight_transpose ; aesop; + replace weight_coweight_transpose := congr_arg ( fun f => f ( Pi.single x_1 1 ) ) weight_coweight_transpose ; aesop; + simp_all +decide [ RootPairingTypeA ]; + simp_all +decide [ TypeA.pairing ]; + simp_all +decide [ Pi.single_apply ]; + grind; + · -- Since the root function is injective, we can conclude that indexEquiv is the identity permutation. + have h_inj : Function.Injective (RootPairingTypeA n).root := by + exact?; + exact Equiv.ext fun x => h_inj <| by simpa using congr_fun root_weightMap.symm x; + refine' ⟨ _, h_surjective ⟩; + exact? + + /- + The homomorphism from the Weyl group of type A to the symmetric group is surjective. + -/ + variable (n : ℕ) + + theorem weylToPermHom_surjective : Function.Surjective (weylToPermHom n) := by + -- Since the homomorphism is bijective, it is surjective. + apply Function.Bijective.surjective; exact weylToPermHom_bijective n + + /- + If an element of the Weyl group acts as the identity on the basis vectors, then it is the identity element. This proves the action is faithful. + -/ + variable (n : ℕ) + + lemma weyl_group_faithful (w : WeylGroupTypeA n) (h : ∀ k, w.val.weightMap (Pi.single k 1) = Pi.single k 1) : w = 1 := by + -- Since the homomorphism is bijective, if it's the identity, the element must be the identity. + have h_bijective : Function.Bijective (weylToPermHom n) := by + exact?; + have h_eq_1 : weylToPermHom n w = 1 := by + ext k; + have := weylToPerm_apply n w k; aesop; + replace this := congr_fun this ( weylToPerm n ⟨ val, property ⟩ k ) ; aesop; + rw [ Pi.single_apply ] at this ; aesop; + exact congr_arg Fin.val this; + exact h_bijective.injective <| by simpa using h_eq_1; + + /- + The cardinality of the Weyl group for the root system A_n is (n+1)!. We prove this by establishing a bijection with the symmetric group S_{n+1}. + -/ + variable (n : ℕ) + + theorem card_WeylGroupTypeA : Nat.card (WeylGroupTypeA n) = (n + 1).factorial := by + have h_bij : Function.Bijective (weylToPermHom n) := weylToPermHom_bijective n + have h_equiv : WeylGroupTypeA n ≃ Equiv.Perm (Fin (n + 1)) := Equiv.ofBijective (weylToPermHom n) h_bij + rw [Nat.card_congr h_equiv] + rw [Nat.card_perm] + simp + + /- + The homomorphism from the Weyl group of type A to the symmetric group is injective. + -/ + variable (n : ℕ) + + theorem weylToPermHom_injective : Function.Injective (weylToPermHom n) := by + -- Since the homomorphism is bijective, it is injective. + apply (weylToPermHom_bijective n).injective + + /- + If an element of the Weyl group acts as the identity on the basis vectors, then it is the identity element. This proves the action is faithful. + -/ + variable (n : ℕ) + + lemma weyl_group_faithful' (w : WeylGroupTypeA n) (h : ∀ k, w.val.weightMap (Pi.single k 1) = Pi.single k 1) : w = 1 := by + exact? + + /- + The Weyl group of type A_n is finite, and its cardinality is (n+1)!. + -/ + variable (n : ℕ) + + instance instFiniteWeylGroupTypeA : Finite (WeylGroupTypeA n) := Finite.of_injective (weylToPermHom n) (weylToPermHom_injective n) + + theorem card_WeylGroupTypeA_eq_fact : Nat.card (WeylGroupTypeA n) = (n + 1).factorial := by + exact?
• SphericalCoord.lean (new)
  • @@ -0,0 +1,109 @@
    + /- + Copyright (c) 2025 Anthony Wang. All rights reserved. + Released under Apache 2.0 license as described in the file LICENSE. + Authors: Anthony Wang + -/ + import Mathlib + + /-! + # Spherical coordinates + + We define spherical coordinates similarly to polar coordinates, as an open partial homeomorphism + in `ℝ^3` between `ℝ^3 - (-∞, 0]` and `(0, +∞) × (-π, π) × (0, π)`. Its inverse is given by + `(r, θ, φ) ↦ (r sin φ cos θ, r sin φ sin θ, r cos φ)`. TODO + + It satisfies the following change of variables formula (see `integral_comp_sphericalCoord_symm`): + `∫ p in sphericalCoord.target, p.1 • f (sphericalCoord.symm p) = ∫ p, f p` + + -/ + + theorem arg_of_im_pos' {z : ℂ} (hz : 0 < z.im) : 0 < Complex.arg z := by + have h₀ : z ≠ 0 := Ne.symm (mt (congr_arg Complex.im) hz.ne) + suffices 0 < Real.sin z.arg by + contrapose! this + exact Real.sin_nonpos_of_nonnpos_of_neg_pi_le this (by linarith [Complex.neg_pi_lt_arg z]) + simp only [Complex.sin_arg, lt_div_iff₀ (norm_pos_iff.mpr h₀), zero_mul, hz] + + + noncomputable section Real + + open Real Set MeasureTheory + + open scoped ENNReal Real Topology + + /-- The spherical coordinates are an open partial homeomorphism in `ℝ^3`, mapping `(r sin φ cos θ, r sin φ sin θ, r cos φ)` to + `(r, θ, φ)`. It is a homeomorphism between `ℝ^3 - (-∞, 0]` and `(0, +∞) × (-π, π) × (0, π)`. TODO -/ + def sphericalCoord : PartialHomeomorph (ℝ × ℝ × ℝ) (ℝ × ℝ × ℝ) where + toFun q := (√(q.1 ^ 2 + q.2.1 ^ 2 + q.2.2 ^ 2), Complex.arg (Complex.equivRealProd.symm (q.1, q.2.1)), Complex.arg (Complex.equivRealProd.symm (q.2.2, √(q.1 ^ 2 + q.2.1 ^ 2)))) + invFun p := (p.1 * sin p.2.2 * cos p.2.1, p.1 * sin p.2.2 * sin p.2.1, p.1 * cos p.2.2) + source := {q | 0 < q.1} ∪ {q | q.2.1 ≠ 0} + target := Ioi (0 : ℝ) ×ˢ Ioo (-π) π ×ˢ Ioo 0 π + map_target' := by + rintro ⟨r, θ, φ⟩ ⟨hr, hθ, hφ⟩ + dsimp at hr hθ hφ + rcases eq_or_ne θ 0 with (rfl | h'θ) + · simp only [ne_eq, cos_zero, mul_one, sin_zero, mul_zero, mem_union, mem_setOf_eq] + left + exact Left.mul_pos hr (sin_pos_of_mem_Ioo hφ) + · simp only [ne_eq, mem_union, mem_setOf_eq, mul_eq_zero, not_or] + right + and_intros + · linarith [mem_Ioi.mp hr] + · linarith [sin_pos_of_mem_Ioo hφ] + · simp [sin_eq_zero_iff_of_lt_of_lt hθ.1 hθ.2, h'θ] + map_source' := by + rintro ⟨x, y, z⟩ hxy + simp only [prodMk_mem_set_prod_eq, mem_Ioi, sqrt_pos, mem_Ioo, Complex.neg_pi_lt_arg, + true_and, Complex.arg_lt_pi_iff] + simp + have hpos : 0 < x ^ 2 + y ^ 2 := by + rcases hxy with hxy | hxy + · dsimp at hxy; linarith [sq_pos_of_ne_zero hxy.ne', sq_nonneg y] + · linarith [sq_nonneg x, sq_pos_of_ne_zero hxy] + and_intros + · rcases hxy with hxy | hxy + · dsimp at hxy; linarith [sq_pos_of_ne_zero hxy.ne', sq_nonneg y, sq_nonneg z] + · linarith [sq_nonneg x, sq_pos_of_ne_zero hxy, sq_nonneg z] + · rcases hxy with hxy | hxy + · exact Or.inl (le_of_lt hxy) + · exact Or.inr hxy + · apply arg_of_im_pos' + simp [hpos] + · exact Or.inr (by simp only [sqrt_ne_zero', hpos]) + right_inv' := by + rintro ⟨r, θ, φ⟩ ⟨hr, hθ, hφ⟩ + ext <;> dsimp at hr hθ hφ ⊢ + · conv_rhs => rw [← sqrt_sq (le_of_lt hr), ← one_mul (r ^ 2), ← sin_sq_add_cos_sq φ, ← one_mul (sin φ ^ 2), ← sin_sq_add_cos_sq θ] + congr 1 + ring + · convert Complex.arg_mul_cos_add_sin_mul_I (Left.mul_pos hr (sin_pos_of_mem_Ioo hφ)) ⟨hθ.1, hθ.2.le⟩ + simp only [Complex.equivRealProd_symm_apply, Complex.ofReal_mul, Complex.ofReal_sin, + Complex.ofReal_cos] + ring + · have : -π < φ := by linarith [pi_pos, hφ.1] + convert Complex.arg_mul_cos_add_sin_mul_I hr ⟨this, hφ.2.le⟩ + have : √((r * sin φ * cos θ) ^ 2 + (r * sin φ * sin θ) ^ 2) = r * sin φ := by + conv_rhs => rw [← sqrt_sq (le_of_lt (Left.mul_pos hr (sin_pos_of_mem_Ioo hφ))), ← one_mul ((r * sin φ) ^ 2), ← sin_sq_add_cos_sq θ] + congr 1 + ring + simp only [this, Complex.equivRealProd_symm_apply, Complex.ofReal_mul, Complex.ofReal_cos, + Complex.ofReal_sin] + ring + left_inv' := by + rintro ⟨x, y, z⟩ _ + -- have A : √(x ^ 2 + y ^ 2) = ‖x + y * Complex.I‖ := by + -- rw [Complex.norm_def, Complex.normSq_add_mul_I] + -- have B : √(x ^ 2 + y ^ 2 + z ^ 2) = ‖z + √(x ^ 2 + y ^ 2) * Complex.I‖ := by + -- rw [Complex.norm_def, Complex.normSq_add_mul_I] + simp -- [Complex.sin_arg] + and_intros + · sorry + · sorry + · sorry + open_target := isOpen_Ioi.prod (isOpen_Ioo.prod isOpen_Ioo) + open_source := + (isOpen_lt continuous_const continuous_fst).union + (isOpen_ne_fun (Continuous.fst continuous_snd) continuous_const) + continuousOn_invFun := by fun_prop + continuousOn_toFun := by + sorry
• SphericalCoord_aristotle.lean (new)
  • @@ -0,0 +1,187 @@
    + /- + This file was edited by Aristotle. + + Lean Toolchain version: leanprover/lean4:v4.20.0-rc5 + Mathlib version: d62eab0cc36ea522904895389c301cf8d844fd69 (May 9, 2025) + + Your Lean code is run in a custom environment, which uses these headers: + + set_option maxHeartbeats 0 + set_option maxRecDepth 4000 + set_option synthInstance.maxHeartbeats 20000 + set_option synthInstance.maxSize 128 + + The following was proved by Aristotle: + + - def sphericalCoord : PartialHomeomorph (ℝ × ℝ × ℝ) (ℝ × ℝ × ℝ) where + toFun q + -/ + + /- + Copyright (c) 2025 Anthony Wang. All rights reserved. + Released under Apache 2.0 license as described in the file LICENSE. + Authors: Anthony Wang + -/ + import Mathlib + + + /-! + # Spherical coordinates + + We define spherical coordinates similarly to polar coordinates, as an open partial homeomorphism + in `ℝ^3` between `ℝ^3 - (-∞, 0]` and `(0, +∞) × (-π, π) × (0, π)`. Its inverse is given by + `(r, θ, φ) ↦ (r sin φ cos θ, r sin φ sin θ, r cos φ)`. TODO + + It satisfies the following change of variables formula (see `integral_comp_sphericalCoord_symm`): + `∫ p in sphericalCoord.target, p.1 • f (sphericalCoord.symm p) = ∫ p, f p` + + -/ + + theorem arg_of_im_pos' {z : ℂ} (hz : 0 < z.im) : 0 < Complex.arg z := by + have h₀ : z ≠ 0 := Ne.symm (mt (congr_arg Complex.im) hz.ne) + suffices 0 < Real.sin z.arg by + contrapose! this + exact Real.sin_nonpos_of_nonnpos_of_neg_pi_le this (by linarith [Complex.neg_pi_lt_arg z]) + simp only [Complex.sin_arg, lt_div_iff₀ (norm_pos_iff.mpr h₀), zero_mul, hz] + + noncomputable section Real + + open Real Set MeasureTheory + + open scoped ENNReal Real Topology + + /-- The spherical coordinates are an open partial homeomorphism in `ℝ^3`, mapping `(r sin φ cos θ, r sin φ sin θ, r cos φ)` to + `(r, θ, φ)`. It is a homeomorphism between `ℝ^3 - (-∞, 0]` and `(0, +∞) × (-π, π) × (0, π)`. TODO -/ + def sphericalCoord : PartialHomeomorph (ℝ × ℝ × ℝ) (ℝ × ℝ × ℝ) where + toFun q := (√(q.1 ^ 2 + q.2.1 ^ 2 + q.2.2 ^ 2), Complex.arg (Complex.equivRealProd.symm (q.1, q.2.1)), Complex.arg (Complex.equivRealProd.symm (q.2.2, √(q.1 ^ 2 + q.2.1 ^ 2)))) + invFun p := (p.1 * sin p.2.2 * cos p.2.1, p.1 * sin p.2.2 * sin p.2.1, p.1 * cos p.2.2) + source := {q | 0 < q.1} ∪ {q | q.2.1 ≠ 0} + target := Ioi (0 : ℝ) ×ˢ Ioo (-π) π ×ˢ Ioo 0 π + map_target' := by + rintro ⟨r, θ, φ⟩ ⟨hr, hθ, hφ⟩ + dsimp at hr hθ hφ + rcases eq_or_ne θ 0 with (rfl | h'θ) + · simp only [ne_eq, cos_zero, mul_one, sin_zero, mul_zero, mem_union, mem_setOf_eq] + left + exact Left.mul_pos hr (sin_pos_of_mem_Ioo hφ) + · simp only [ne_eq, mem_union, mem_setOf_eq, mul_eq_zero, not_or] + right + and_intros + · linarith [mem_Ioi.mp hr] + · linarith [sin_pos_of_mem_Ioo hφ] + · simp [sin_eq_zero_iff_of_lt_of_lt hθ.1 hθ.2, h'θ] + map_source' := by + rintro ⟨x, y, z⟩ hxy + simp only [prodMk_mem_set_prod_eq, mem_Ioi, sqrt_pos, mem_Ioo, Complex.neg_pi_lt_arg, + true_and, Complex.arg_lt_pi_iff] + simp + have hpos : 0 < x ^ 2 + y ^ 2 := by + rcases hxy with hxy | hxy + · dsimp at hxy; linarith [sq_pos_of_ne_zero hxy.ne', sq_nonneg y] + · linarith [sq_nonneg x, sq_pos_of_ne_zero hxy] + and_intros + · rcases hxy with hxy | hxy + · dsimp at hxy; linarith [sq_pos_of_ne_zero hxy.ne', sq_nonneg y, sq_nonneg z] + · linarith [sq_nonneg x, sq_pos_of_ne_zero hxy, sq_nonneg z] + · rcases hxy with hxy | hxy + · exact Or.inl (le_of_lt hxy) + · exact Or.inr hxy + · apply arg_of_im_pos' + simp [hpos] + · exact Or.inr (by simp only [sqrt_ne_zero', hpos]) + right_inv' := by + rintro ⟨r, θ, φ⟩ ⟨hr, hθ, hφ⟩ + ext <;> dsimp at hr hθ hφ ⊢ + · conv_rhs => rw [← sqrt_sq (le_of_lt hr), ← one_mul (r ^ 2), ← sin_sq_add_cos_sq φ, ← one_mul (sin φ ^ 2), ← sin_sq_add_cos_sq θ] + congr 1 + ring + · convert Complex.arg_mul_cos_add_sin_mul_I (Left.mul_pos hr (sin_pos_of_mem_Ioo hφ)) ⟨hθ.1, hθ.2.le⟩ + simp only [Complex.equivRealProd_symm_apply, Complex.ofReal_mul, Complex.ofReal_sin, + Complex.ofReal_cos] + ring + · have : -π < φ := by linarith [pi_pos, hφ.1] + convert Complex.arg_mul_cos_add_sin_mul_I hr ⟨this, hφ.2.le⟩ + have : √((r * sin φ * cos θ) ^ 2 + (r * sin φ * sin θ) ^ 2) = r * sin φ := by + conv_rhs => rw [← sqrt_sq (le_of_lt (Left.mul_pos hr (sin_pos_of_mem_Ioo hφ))), ← one_mul ((r * sin φ) ^ 2), ← sin_sq_add_cos_sq θ] + congr 1 + ring + simp only [this, Complex.equivRealProd_symm_apply, Complex.ofReal_mul, Complex.ofReal_cos, + Complex.ofReal_sin] + ring + left_inv' := by + rintro ⟨x, y, z⟩ _ + -- have A : √(x ^ 2 + y ^ 2) = ‖x + y * Complex.I‖ := by + -- rw [Complex.norm_def, Complex.normSq_add_mul_I] + -- have B : √(x ^ 2 + y ^ 2 + z ^ 2) = ‖z + √(x ^ 2 + y ^ 2) * Complex.I‖ := by + -- rw [Complex.norm_def, Complex.normSq_add_mul_I] + simp -- [Complex.sin_arg] + and_intros + · + rw [ Complex.sin_arg, Complex.cos_arg ] <;> aesop; + · -- Simplify the expression by canceling out the common terms. + field_simp [Complex.normSq, Complex.norm_def] + ring; + field_simp [mul_comm, mul_assoc, mul_left_comm]; + · norm_num [ Complex.normSq, Complex.norm_def ] ; ring; + -- By simplifying, we can see that the expression indeed equals $x$. + field_simp + ring; + · -- From the equation $x + y * Complex.I = 0$, we can separate the real and imaginary parts to get $x = 0$ and $y = 0$. + have h_real_imag : x = 0 ∧ y = 0 := by + -- Since $x + y * Complex.I = 0$, we can separate the real and imaginary parts to get $x = 0$ and $y = 0$. + simp [Complex.ext_iff] at a_1; exact ⟨by linarith, by linarith⟩; + -- Since $x = 0$ and $0 < x$, this is a contradiction. + aesop; + · simp_all +decide [ Complex.ext_iff ] + · + rw [ Complex.sin_arg, Complex.sin_arg ] <;> aesop; + · -- Simplify the norms and cancel out the common terms. + field_simp [Complex.normSq, Complex.norm_def] + ring; + -- By simplifying, we can see that the expression indeed equals y. + field_simp [mul_comm, mul_assoc, mul_left_comm]; + · -- Simplify the norms and square roots in the expression. + field_simp [Complex.normSq, Complex.norm_def] + ring; + simp +decide [ mul_assoc, mul_comm, mul_left_comm, ne_of_gt ( Real.sqrt_pos.mpr ( show 0 < x ^ 2 + y ^ 2 + z ^ 2 by positivity ) ), ne_of_gt ( Real.sqrt_pos.mpr ( show 0 < x ^ 2 + y ^ 2 by positivity ) ) ] + · + rw [ Complex.cos_arg ] <;> aesop; + · norm_num [ Complex.normSq, Complex.norm_def ]; + rw [ Real.mul_self_sqrt ( by positivity ) ] ; ring_nf; + rw [ mul_assoc, mul_inv_cancel₀ ( by positivity ), mul_one ]; + · norm_num [ Complex.normSq, Complex.norm_def ]; + rw [ Real.mul_self_sqrt ( by positivity ) ] ; ring; + rw [ mul_assoc, mul_inv_cancel₀ ( by positivity ), mul_one ]; + · -- Since $z$ is real and $\sqrt{x^2 + y^2}$ is real, the only way their sum can be zero is if both parts are zero. However, $\sqrt{x^2 + y^2}$ is always non-negative and since $x$ is positive, it can't be zero. Therefore, $z$ must be zero, but then the imaginary part would be $\sqrt{x^2 + y^2}$, which can't be zero either. This leads to a contradiction. + have h_contra : z = 0 ∧ Real.sqrt (x^2 + y^2) = 0 := by + simp_all +decide [ Complex.ext_iff ]; + exact absurd h_contra.2 ( by positivity ); + · simp_all +decide [ Complex.ext_iff ]; + exact ne_of_gt ( Real.sqrt_pos.mpr ( by positivity ) ) a_1.2 + open_target := isOpen_Ioi.prod (isOpen_Ioo.prod isOpen_Ioo) + open_source := + (isOpen_lt continuous_const continuous_fst).union + (isOpen_ne_fun (Continuous.fst continuous_snd) continuous_const) + continuousOn_invFun := by fun_prop + continuousOn_toFun := by + refine' ContinuousOn.prod _ _; + · exact Continuous.continuousOn ( Real.continuous_sqrt.comp <| Continuous.add ( Continuous.add ( continuous_fst.pow 2 ) ( continuous_snd.fst.pow 2 ) ) ( continuous_snd.snd.pow 2 ) ); + · field_simp; + -- The argument function is continuous except at zero, and since the inputs are never zero in the given set, the argument function is continuous. + have h_arg_cont : ContinuousOn (fun q : ℝ × ℝ × ℝ => Complex.arg (q.1 + q.2.1 * Complex.I)) ({q : ℝ × ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ × ℝ | ¬q.2.1 = 0}) ∧ ContinuousOn (fun q : ℝ × ℝ × ℝ => Complex.arg (q.2.2 + Real.sqrt (q.1^2 + q.2.1^2) * Complex.I)) ({q : ℝ × ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ × ℝ | ¬q.2.1 = 0}) := by + constructor <;> refine' ContinuousAt.continuousOn _ <;> intro q hq <;> aesop; + · refine' Complex.continuousAt_arg _ |> fun h => h.comp _; + · simp [Complex.slitPlane, h]; + · fun_prop (disch := norm_num); + · refine' Complex.continuousAt_arg _ |> fun h => h.comp _; + · simp [Complex.slitPlane, h_1]; + · fun_prop (disch := norm_num); + · refine' Complex.continuousAt_arg _ |> ContinuousAt.comp <| _; + · norm_num [ Complex.slitPlane, Complex.ext_iff ]; + exact Or.inr ( ne_of_gt ( Real.sqrt_pos.mpr ( by positivity ) ) ); + · fun_prop; + · refine' Complex.continuousAt_arg _ |> fun h => h.comp _; + · norm_num [ Complex.slitPlane ]; + exact Or.inr ( ne_of_gt ( Real.sqrt_pos.mpr ( by positivity ) ) ); + · fun_prop (disch := norm_num); + exact ContinuousOn.prod h_arg_cont.1 h_arg_cont.2