-- Mathlib/NumberTheory/NumberField/House.lean
theorem basis_repr_norm_le_const_mul_house (α : 𝓞 K) (i : K →+* ℂ) :
    ‖(((integralBasis K).reindex (equivReindex K).symm).repr α i : ℂ)‖  ≤
      (c K) * house (algebraMap (𝓞 K) K α)

Proof state:
case calc_3
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ∑ x : K →+* ℂ, ‖fun i j => (basisMatrix K)ᵀ⁻¹ i j‖ * house ((algebraMap (𝓞 K) K) α) =
    ↑(finrank ℚ K) * ‖(basisMatrix K)ᵀ⁻¹‖ * house ((algebraMap (𝓞 K) K) α)

Tactic:
rw [sum_const, card_univ, nsmul_eq_mul, Embeddings.card, mul_assoc]

Result:
no goals

Proof state:
case calc_1
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ‖((basisMatrix K)ᵀ⁻¹ *ᵥ fun j => (canonicalEmbedding K) ((algebraMap (𝓞 K) K) α) j) i‖ ≤
    ∑ j : K →+* ℂ, ‖(basisMatrix K)ᵀ⁻¹‖ * ‖σ ((algebraMap (𝓞 K) K) α) j‖

Tactic:
apply le_trans

Result:
case calc_1.a
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ‖((basisMatrix K)ᵀ⁻¹ *ᵥ fun j => (canonicalEmbedding K) ((algebraMap (𝓞 K) K) α) j) i‖ ≤ ?calc_1.b

case calc_1.a
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ?calc_1.b ≤ ∑ j : K →+* ℂ, ‖(basisMatrix K)ᵀ⁻¹‖ * ‖σ ((algebraMap (𝓞 K) K) α) j‖

case calc_1.b
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ℝ

Proof state:
case calc_1
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ‖↑((((integralBasis K).reindex (equivReindex K).symm).repr ↑α) i)‖ ≤
    ∑ j : K →+* ℂ, ‖(basisMatrix K)ᵀ⁻¹‖ * ‖σ ((algebraMap (𝓞 K) K) α) j‖

Tactic:
rw [← inverse_basisMatrix_mulVec_eq_repr]

Result:
case calc_1
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ‖((basisMatrix K)ᵀ⁻¹ *ᵥ fun j => (canonicalEmbedding K) ((algebraMap (𝓞 K) K) α) j) i‖ ≤
    ∑ j : K →+* ℂ, ‖(basisMatrix K)ᵀ⁻¹‖ * ‖σ ((algebraMap (𝓞 K) K) α) j‖

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ‖↑((((integralBasis K).reindex (equivReindex K).symm).repr ↑α) i)‖ ≤
    NumberField.house.c K * house ((algebraMap (𝓞 K) K) α)

Tactic:
calc
  _ ≤ ∑ j, ‖((basisMatrix K).transpose)⁻¹‖ * ‖σ (algebraMap (𝓞 K) K α) j‖  := ?_
  _ ≤ ∑ _ : K →+* ℂ, ‖fun i j => ((basisMatrix K).transpose)⁻¹ i j‖
      * house (algebraMap (𝓞 K) K α) := ?_
  _ = ↑(finrank ℚ K) * ‖((basisMatrix K).transpose)⁻¹‖ * house (algebraMap (𝓞 K) K α) := ?_

Result:
case calc_1
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ‖↑((((integralBasis K).reindex (equivReindex K).symm).repr ↑α) i)‖ ≤
    ∑ j : K →+* ℂ, ‖(basisMatrix K)ᵀ⁻¹‖ * ‖σ ((algebraMap (𝓞 K) K) α) j‖

case calc_2
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ∑ j : K →+* ℂ, ‖(basisMatrix K)ᵀ⁻¹‖ * ‖σ ((algebraMap (𝓞 K) K) α) j‖ ≤
    ∑ x : K →+* ℂ, ‖fun i j => (basisMatrix K)ᵀ⁻¹ i j‖ * house ((algebraMap (𝓞 K) K) α)

case calc_3
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ∑ x : K →+* ℂ, ‖fun i j => (basisMatrix K)ᵀ⁻¹ i j‖ * house ((algebraMap (𝓞 K) K) α) =
    ↑(finrank ℚ K) * ‖(basisMatrix K)ᵀ⁻¹‖ * house ((algebraMap (𝓞 K) K) α)

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
x✝¹ : K →+* ℂ
x✝ : x✝¹ ∈ univ
⊢ ‖(fun j => (basisMatrix K)ᵀ⁻¹ i j) x✝¹‖ ≤ ‖(basisMatrix K)ᵀ⁻¹‖

Tactic:
exact norm_entry_le_entrywise_sup_norm ((basisMatrix K).transpose)⁻¹

Result:
no goals

Proof state:
case calc_1.a
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ∑ i_1 : K →+* ℂ,
      ‖(fun j => (basisMatrix K)ᵀ⁻¹ i j) i_1‖ * ‖(fun j => (canonicalEmbedding K) ((algebraMap (𝓞 K) K) α) j) i_1‖ ≤
    ∑ j : K →+* ℂ, ‖(basisMatrix K)ᵀ⁻¹‖ * ‖σ ((algebraMap (𝓞 K) K) α) j‖

Tactic:
apply sum_le_sum fun _ _ => mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)

Result:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
x✝¹ : K →+* ℂ
x✝ : x✝¹ ∈ univ
⊢ ‖(fun j => (basisMatrix K)ᵀ⁻¹ i j) x✝¹‖ ≤ ‖(basisMatrix K)ᵀ⁻¹‖

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
⊢ ‖↑((((integralBasis K).reindex (equivReindex K).symm).repr ↑α) i)‖ ≤
    NumberField.house.c K * house ((algebraMap (𝓞 K) K) α)

Tactic:
let σ := canonicalEmbedding K

Result:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ‖↑((((integralBasis K).reindex (equivReindex K).symm).repr ↑α) i)‖ ≤
    NumberField.house.c K * house ((algebraMap (𝓞 K) K) α)

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
j : K →+* ℂ
a✝ : j ∈ univ
⊢ ‖σ ((algebraMap (𝓞 K) K) α) j‖ ≤ house ((algebraMap (𝓞 K) K) α)

Tactic:
exact norm_le_pi_norm (σ ((algebraMap (𝓞 K) K) α)) j

Result:
no goals

Proof state:
case calc_1.a
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ‖((basisMatrix K)ᵀ⁻¹ *ᵥ fun j => (canonicalEmbedding K) ((algebraMap (𝓞 K) K) α) j) i‖ ≤ ?calc_1.b

Tactic:
apply le_trans (norm_sum_le _ _)

Result:
case calc_1.a
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ∑ i_1 : K →+* ℂ,
      ‖(fun j => (basisMatrix K)ᵀ⁻¹ i j) i_1 * (fun j => (canonicalEmbedding K) ((algebraMap (𝓞 K) K) α) j) i_1‖ ≤
    ?calc_1.b

case calc_1.b
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ℝ

Proof state:
case calc_2.h
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
j : K →+* ℂ
a✝ : j ∈ univ
⊢ ‖(basisMatrix K)ᵀ⁻¹‖ * ‖σ ((algebraMap (𝓞 K) K) α) j‖ ≤
    ‖fun i j => (basisMatrix K)ᵀ⁻¹ i j‖ * house ((algebraMap (𝓞 K) K) α)

Tactic:
apply mul_le_mul_of_nonneg_left _ (norm_nonneg fun i j ↦ ((basisMatrix K).transpose)⁻¹ i j)

Result:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
j : K →+* ℂ
a✝ : j ∈ univ
⊢ ‖σ ((algebraMap (𝓞 K) K) α) j‖ ≤ house ((algebraMap (𝓞 K) K) α)

Proof state:
case calc_1.a
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ∑ i_1 : K →+* ℂ,
      ‖(fun j => (basisMatrix K)ᵀ⁻¹ i j) i_1 * (fun j => (canonicalEmbedding K) ((algebraMap (𝓞 K) K) α) j) i_1‖ ≤
    ?calc_1.b

Tactic:
exact sum_le_sum fun _ _ => (norm_mul _ _).le

Result:
no goals