Skip to content

Commit

Permalink
p1~2 done; todo simplify
Browse files Browse the repository at this point in the history
  • Loading branch information
@cadake
cadake committed Oct 16, 2024
1 parent 82f777d commit 7a984a2
Showing 1 changed file with 165 additions and 124 deletions.
289 changes: 165 additions & 124 deletions LeanTQI/VectorNorm.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -645,133 +645,174 @@ example (ple2 : p ≤ 2) (h : p ≠ ⊤) : LpNorm p (A * B) ≤ (LpNorm p A) * (
have pinvpos : 0 < p.toReal⁻¹ := inv_pos_of_pos ppos
rw [← Real.mul_rpow Apnn Bpnn, Real.rpow_le_rpow_iff ABpnn ApBpnn pinvpos]

have : ∀ (i : m) (j : l), ‖(A * B) i j‖ ≤ ∑ (k : n), ‖A i k‖ * ‖B k j‖ := by
intro i j
simp [Matrix.mul_apply]
exact norm_sum_le_of_le Finset.univ (fun k kin => NormedRing.norm_mul (A i k) (B k j))

-- by_cases hp : p = 1
-- · simp only [hp, ENNReal.one_toReal, Real.rpow_one, ge_iff_le]
by_cases hp : p.toReal = 1
· sorry
let q := p.toReal.conjExponent
have hpq : p.toReal.IsConjExponent q := by
refine Real.IsConjExponent.conjExponent ?h
have : 1 ≤ p.toReal := by
cases ENNReal.dichotomy p
· contradiction
assumption
exact lt_of_le_of_ne this fun a ↦ hp (id (Eq.symm a))
have s : Finset n := Finset.univ
calc
∑ i : m, ∑ j : l, ‖(A * B) i j‖ ^ p.toReal ≤ ∑ i, ∑ j, (∑ (k : n), ‖A i k‖ * ‖B k j‖) ^ p.toReal := by
apply Finset.sum_le_sum
intro i iin
apply Finset.sum_le_sum
intro j jin
rw [Real.rpow_le_rpow_iff (norm_nonneg <| (A * B) i j)
(Finset.sum_nonneg fun k _ => mul_nonneg (norm_nonneg (A i k)) (norm_nonneg (B k j))) ppos]
exact this i j
_ ≤ ∑ i, ∑ j, ((∑ (k : n), ‖A i k‖ ^ p.toReal) ^ p.toReal⁻¹ * (∑ k, ‖B k j‖ ^ q) ^ q⁻¹) ^ p.toReal := by
apply Finset.sum_le_sum
intro i iin
apply Finset.sum_le_sum
intro j jin
have : 0 ≤ (∑ k : n, ‖A i k‖ ^ p.toReal) ^ p.toReal⁻¹ * (∑ k : n, ‖B k j‖ ^ q) ^ q⁻¹ :=
Left.mul_nonneg (Real.rpow_nonneg (Finset.sum_nonneg (fun k _ => Real.rpow_nonneg (norm_nonneg (A i k)) p.toReal)) p.toReal⁻¹)
(Real.rpow_nonneg (Finset.sum_nonneg (fun k _ => Real.rpow_nonneg (norm_nonneg (B k j)) q)) q⁻¹)
rw [Real.rpow_le_rpow_iff (Finset.sum_nonneg fun k _ => mul_nonneg (norm_nonneg (A i k)) (norm_nonneg (B k j)))
this ppos]
rw [← one_div, ← one_div]
conv_rhs =>
enter [1, 1, 2]
intro k
enter [1]
rw [Eq.symm (abs_norm (A i k))]
conv_rhs =>
enter [2, 1, 2]
intro k
enter [1]
rw [Eq.symm (abs_norm (B k j))]
exact Real.inner_le_Lp_mul_Lq (f := fun k => ‖A i k‖) (g := fun k => ‖B k j‖) (hpq := hpq) (Finset.univ)
_ = ∑ i, ∑ j, (∑ (k : n), ‖A i k‖ ^ p.toReal) * ((∑ k, ‖B k j‖ ^ q) ^ q⁻¹) ^ p.toReal := by
conv_lhs =>
enter [2]
intro i
conv =>
-- simp only [hp, Real.rpow_one]
case pos =>
calc
∑ i : m, ∑ j : l, ‖(A * B) i j‖ ^ p.toReal ≤ ∑ i, ∑ j, (∑ (k : n), ‖A i k‖ * ‖B k j‖) ^ p.toReal := by
-- todo : extract
apply Finset.sum_le_sum
intro i _
apply Finset.sum_le_sum
intro j _
rw [Real.rpow_le_rpow_iff (norm_nonneg <| (A * B) i j)
(Finset.sum_nonneg fun k _ => mul_nonneg (norm_nonneg (A i k)) (norm_nonneg (B k j))) ppos]
have : ∀ (i : m) (j : l), ‖(A * B) i j‖ ≤ ∑ (k : n), ‖A i k‖ * ‖B k j‖ := by
intro i j
simp [Matrix.mul_apply]
exact norm_sum_le_of_le Finset.univ (fun k _ => NormedRing.norm_mul (A i k) (B k j))
exact this i j
_ = ∑ k : n, ∑ i : m, ∑ j : l, ‖A i k‖ * ‖B k j‖ := by
simp only [hp, Real.rpow_one]
conv_lhs =>
enter [2]
intro j
rw [Real.mul_rpow (Real.rpow_nonneg (Arpnn i) p.toReal⁻¹)
(Real.rpow_nonneg (Finset.sum_nonneg (fun i _ => Real.rpow_nonneg (norm_nonneg (B i j)) q)) q⁻¹),
← Real.rpow_mul <| Arpnn i, inv_mul_cancel₀ <| ENNReal.ge_one_toReal_ne_zero p h, Real.rpow_one]
_ = (∑ i, ∑ (k : n), (‖A i k‖ ^ p.toReal)) * (∑ j, ((∑ k, ‖B k j‖ ^ q) ^ q⁻¹) ^ p.toReal) := by
rw [← Finset.sum_mul_sum Finset.univ Finset.univ (fun i => ∑ (k : n), (‖A i k‖ ^ p.toReal)) (fun j => ((∑ k, ‖B k j‖ ^ q) ^ q⁻¹) ^ p.toReal)]
_ ≤ (∑ i : m, ∑ j : n, ‖A i j‖ ^ p.toReal) * ∑ i : n, ∑ j : l, ‖B i j‖ ^ p.toReal := by
by_cases h' : ∑ i : m, ∑ k : n, ‖A i k‖ ^ p.toReal = 0
· simp only [h', zero_mul, le_refl]
have h' : 0 < ∑ i : m, ∑ k : n, ‖A i k‖ ^ p.toReal := by
have : 0 ≤ ∑ i : m, ∑ k : n, ‖A i k‖ ^ p.toReal := by
apply Finset.sum_nonneg
intro i iin
apply Finset.sum_nonneg
intro j jin
exact Real.rpow_nonneg (norm_nonneg (A i j)) p.toReal
exact lt_of_le_of_ne Apnn fun a ↦ h' (id (Eq.symm a))
rw [mul_le_mul_left h', Finset.sum_comm]
apply Finset.sum_le_sum
intro i iin
have : ((∑ k : n, ‖B k i‖ ^ q) ^ q⁻¹) ≤ ((∑ k : n, ‖B k i‖ ^ p.toReal) ^ p.toReal⁻¹) := by
have : p.toReal ≤ q := by
sorry

let B' : Matrix n Unit 𝕂 := Matrix.col Unit (fun k : n => B k i)
have : (∑ k : n, ‖B k i‖ ^ q) ^ q⁻¹ = (∑ k : n, ‖B' k ()‖ ^ q) ^ q⁻¹ := by
exact rfl
rw [this]
have : (∑ k : n, ‖B k i‖ ^ p.toReal) ^ p.toReal⁻¹ = (∑ k : n, ‖B' k ()‖ ^ p.toReal) ^ p.toReal⁻¹ := by
exact rfl
rw [this]

have : (∑ k : n, ‖B' k ()‖ ^ q) ^ q⁻¹ = (∑ k : n, ∑ j : Unit, ‖B' k j‖ ^ q) ^ q⁻¹ := by
have : ∀ k : n, ∑ j : Unit, ‖B' k ()‖ ^ q = ‖B' k ()‖ ^ q := by
intro k
exact Fintype.sum_unique fun x ↦ ‖B' k ()‖ ^ q
simp_rw [this]
rw [this]
have : (∑ k : n, ‖B' k ()‖ ^ p.toReal) ^ p.toReal⁻¹ = (∑ k : n, ∑ j : Unit, ‖B' k j‖ ^ p.toReal) ^ p.toReal⁻¹ := by
have : ∀ k : n, ∑ j : Unit, ‖B' k ()‖ ^ p.toReal = ‖B' k ()‖ ^ p.toReal := by
intro k
exact Fintype.sum_unique fun x ↦ ‖B' k ()‖ ^ p.toReal
simp_rw [this]
rw [this]


let q' : ℝ≥0∞ := ENNReal.ofReal q
have hq : q' ≠ ⊤ := ENNReal.ofReal_ne_top
have : q = q'.toReal := by
refine Eq.symm (ENNReal.toReal_ofReal ?h)
exact Real.IsConjExponent.nonneg (id (Real.IsConjExponent.symm hpq))
rw [this, ← one_div, ← one_div]
have inst : Fact (1 ≤ q') := by
refine { out := ?out }
refine ENNReal.one_le_ofReal.mpr ?out.a
rw [show q = p.toReal / (p.toReal - 1) by rfl]
rw [one_le_div_iff]
left
sorry
have pleq : p ≤ q' := by
refine (ENNReal.le_ofReal_iff_toReal_le h ?hb).mpr (by assumption)
exact ENNReal.toReal_ofReal_eq_iff.mp (id (Eq.symm this))


rw [← lp_norm_def q' B' hq, lp_norm_eq_lpnorm, ← lp_norm_def p B' h, lp_norm_eq_lpnorm]
apply lpnorm_antimono B' p q' h hq pleq

refine (Real.le_rpow_inv_iff_of_pos ?_ ?_ ppos).mp this
· exact Real.rpow_nonneg (Finset.sum_nonneg (fun i' _ => Real.rpow_nonneg (norm_nonneg (B i' i)) q)) q⁻¹
exact (Finset.sum_nonneg (fun i' _ => Real.rpow_nonneg (norm_nonneg (B i' i)) p.toReal))

#check Singleton
rw [Finset.sum_comm]
rw [Finset.sum_comm]
_ = ∑ k : n, (∑ i : m, ‖A i k‖) * (∑ j : l, ‖B k j‖) := by
congr
ext k
exact Eq.symm (Fintype.sum_mul_sum (fun i ↦ ‖A i k‖) fun j ↦ ‖B k j‖)
_ ≤ ∑ k : n, (∑ i : m, ‖A i k‖) * ∑ k : n, (∑ j : l, ‖B k j‖) := by
apply Finset.sum_le_sum
intro y yin
by_cases h' : ∑ i : m, ‖A i y‖ = 0
· simp only [h', zero_mul, le_refl]
rw [mul_le_mul_left]
apply Finset.single_le_sum (f := fun (i : n) => ∑ j : l, ‖B i j‖)
(fun i _ => Finset.sum_nonneg (fun j _ => norm_nonneg (B i j))) yin
exact lt_of_le_of_ne (Finset.sum_nonneg (fun i _ => norm_nonneg (A i y)))
fun a ↦ h' (id (Eq.symm a))
_ = (∑ i : m, ∑ j : n, ‖A i j‖ ^ p.toReal) * ∑ i : n, ∑ j : l, ‖B i j‖ ^ p.toReal := by
simp only [hp, Real.rpow_one]
rw [Eq.symm
(Finset.sum_mul Finset.univ (fun i ↦ ∑ i_1 : m, ‖A i_1 i‖) (∑ k : n, ∑ j : l, ‖B k j‖)),
Finset.sum_comm (f := fun i j => ‖A i j‖)]
case neg =>
let q := p.toReal.conjExponent
have hpq : p.toReal.IsConjExponent q := by
apply Real.IsConjExponent.conjExponent
have : 1 ≤ p.toReal := by
cases ENNReal.dichotomy p
· contradiction
assumption
exact lt_of_le_of_ne this fun a ↦ hp (id (Eq.symm a))
let q' : ℝ≥0∞ := ENNReal.ofReal q
have prleq : p.toReal ≤ q := by
rw [Real.IsConjExponent.conj_eq hpq]
apply le_div_self (ENNReal.toReal_nonneg) (Real.IsConjExponent.sub_one_pos hpq)
rw [← add_le_add_iff_right 1]
simp only [sub_add_cancel]
rw [one_add_one_eq_two]
apply ENNReal.toReal_le_of_le_ofReal (by linarith)
rw [show ENNReal.ofReal 2 = (2 : ℝ≥0∞) by exact ENNReal.ofReal_eq_ofNat.mpr rfl]
exact ple2
have hq : q' ≠ ⊤ := ENNReal.ofReal_ne_top
have qeqqr : q = q'.toReal := by
refine Eq.symm (ENNReal.toReal_ofReal ?h)
exact Real.IsConjExponent.nonneg (id (Real.IsConjExponent.symm hpq))
have pleq : p ≤ q' := by
apply (ENNReal.le_ofReal_iff_toReal_le h ?hb).mpr prleq
exact ENNReal.toReal_ofReal_eq_iff.mp (id (Eq.symm qeqqr))

calc
∑ i : m, ∑ j : l, ‖(A * B) i j‖ ^ p.toReal ≤ ∑ i, ∑ j, (∑ (k : n), ‖A i k‖ * ‖B k j‖) ^ p.toReal := by
-- todo : extract
apply Finset.sum_le_sum
intro i _
apply Finset.sum_le_sum
intro j _
rw [Real.rpow_le_rpow_iff (norm_nonneg <| (A * B) i j)
(Finset.sum_nonneg fun k _ => mul_nonneg (norm_nonneg (A i k)) (norm_nonneg (B k j))) ppos]
have : ∀ (i : m) (j : l), ‖(A * B) i j‖ ≤ ∑ (k : n), ‖A i k‖ * ‖B k j‖ := by
intro i j
simp [Matrix.mul_apply]
exact norm_sum_le_of_le Finset.univ (fun k _ => NormedRing.norm_mul (A i k) (B k j))
exact this i j
_ ≤ ∑ i, ∑ j, ((∑ (k : n), ‖A i k‖ ^ p.toReal) ^ p.toReal⁻¹ * (∑ k, ‖B k j‖ ^ q) ^ q⁻¹) ^ p.toReal := by
-- todo : extract
apply Finset.sum_le_sum
intro i _
apply Finset.sum_le_sum
intro j _
have : 0 ≤ (∑ k : n, ‖A i k‖ ^ p.toReal) ^ p.toReal⁻¹ * (∑ k : n, ‖B k j‖ ^ q) ^ q⁻¹ :=
Left.mul_nonneg (Real.rpow_nonneg (Finset.sum_nonneg (fun k _ => Real.rpow_nonneg (norm_nonneg (A i k)) p.toReal)) p.toReal⁻¹)
(Real.rpow_nonneg (Finset.sum_nonneg (fun k _ => Real.rpow_nonneg (norm_nonneg (B k j)) q)) q⁻¹)
rw [Real.rpow_le_rpow_iff (Finset.sum_nonneg fun k _ => mul_nonneg (norm_nonneg (A i k)) (norm_nonneg (B k j)))
this ppos]
rw [← one_div, ← one_div]
conv_rhs =>
enter [1, 1, 2]
intro k
enter [1]
rw [Eq.symm (abs_norm (A i k))]
conv_rhs =>
enter [2, 1, 2]
intro k
enter [1]
rw [Eq.symm (abs_norm (B k j))]
exact Real.inner_le_Lp_mul_Lq (f := fun k => ‖A i k‖) (g := fun k => ‖B k j‖) (hpq := hpq) (Finset.univ)
_ = ∑ i, ∑ j, (∑ (k : n), ‖A i k‖ ^ p.toReal) * ((∑ k, ‖B k j‖ ^ q) ^ q⁻¹) ^ p.toReal := by
conv_lhs =>
enter [2]
intro i
conv =>
enter [2]
intro j
rw [Real.mul_rpow (Real.rpow_nonneg (Arpnn i) p.toReal⁻¹)
(Real.rpow_nonneg (Finset.sum_nonneg (fun i _ => Real.rpow_nonneg (norm_nonneg (B i j)) q)) q⁻¹),
← Real.rpow_mul <| Arpnn i, inv_mul_cancel₀ <| ENNReal.ge_one_toReal_ne_zero p h, Real.rpow_one]
_ = (∑ i, ∑ (k : n), (‖A i k‖ ^ p.toReal)) * (∑ j, ((∑ k, ‖B k j‖ ^ q) ^ q⁻¹) ^ p.toReal) := by
rw [← Finset.sum_mul_sum Finset.univ Finset.univ (fun i => ∑ (k : n), (‖A i k‖ ^ p.toReal)) (fun j => ((∑ k, ‖B k j‖ ^ q) ^ q⁻¹) ^ p.toReal)]
_ ≤ (∑ i : m, ∑ j : n, ‖A i j‖ ^ p.toReal) * ∑ i : n, ∑ j : l, ‖B i j‖ ^ p.toReal := by
by_cases h' : ∑ i : m, ∑ k : n, ‖A i k‖ ^ p.toReal = 0
· simp only [h', zero_mul, le_refl]
have h' : 0 < ∑ i : m, ∑ k : n, ‖A i k‖ ^ p.toReal := by
have : 0 ≤ ∑ i : m, ∑ k : n, ‖A i k‖ ^ p.toReal := by
apply Finset.sum_nonneg
intro i _
apply Finset.sum_nonneg
intro j _
exact Real.rpow_nonneg (norm_nonneg (A i j)) p.toReal
exact lt_of_le_of_ne Apnn fun a ↦ h' (id (Eq.symm a))
rw [mul_le_mul_left h', Finset.sum_comm]
apply Finset.sum_le_sum
intro i _
have : ((∑ k : n, ‖B k i‖ ^ q) ^ q⁻¹) ≤ ((∑ k : n, ‖B k i‖ ^ p.toReal) ^ p.toReal⁻¹) := by
let B' : Matrix n Unit 𝕂 := Matrix.col Unit (fun k : n => B k i)
have : (∑ k : n, ‖B k i‖ ^ q) ^ q⁻¹ = (∑ k : n, ‖B' k ()‖ ^ q) ^ q⁻¹ := by
exact rfl
rw [this]
have : (∑ k : n, ‖B k i‖ ^ p.toReal) ^ p.toReal⁻¹ = (∑ k : n, ‖B' k ()‖ ^ p.toReal) ^ p.toReal⁻¹ := by
exact rfl
rw [this]
have : (∑ k : n, ‖B' k ()‖ ^ q) ^ q⁻¹ = (∑ k : n, ∑ j : Unit, ‖B' k j‖ ^ q) ^ q⁻¹ := by
have : ∀ k : n, ∑ _ : Unit, ‖B' k ()‖ ^ q = ‖B' k ()‖ ^ q := by
intro k
exact Fintype.sum_unique fun _ ↦ ‖B' k ()‖ ^ q
simp_rw [this]
rw [this]
have : (∑ k : n, ‖B' k ()‖ ^ p.toReal) ^ p.toReal⁻¹ = (∑ k : n, ∑ j : Unit, ‖B' k j‖ ^ p.toReal) ^ p.toReal⁻¹ := by
have : ∀ k : n, ∑ _ : Unit, ‖B' k ()‖ ^ p.toReal = ‖B' k ()‖ ^ p.toReal := by
intro k
exact Fintype.sum_unique fun _ ↦ ‖B' k ()‖ ^ p.toReal
simp_rw [this]
rw [this, qeqqr, ← one_div, ← one_div]
have inst : Fact (1 ≤ q') := by
refine { out := ?out }
refine ENNReal.one_le_ofReal.mpr ?out.a
rw [Real.IsConjExponent.conj_eq hpq]
rw [one_le_div_iff]
left
constructor
· exact Real.IsConjExponent.sub_one_pos hpq
· linarith
rw [← lp_norm_def q' B' hq, lp_norm_eq_lpnorm, ← lp_norm_def p B' h, lp_norm_eq_lpnorm]
exact lpnorm_antimono B' p q' h hq pleq
refine (Real.le_rpow_inv_iff_of_pos ?_ ?_ ppos).mp this
· exact Real.rpow_nonneg (Finset.sum_nonneg (fun i' _ => Real.rpow_nonneg (norm_nonneg (B i' i)) q)) q⁻¹
exact (Finset.sum_nonneg (fun i' _ => Real.rpow_nonneg (norm_nonneg (B i' i)) p.toReal))




Expand Down

0 comments on commit 7a984a2

Please sign in to comment.