From c335cd88ef47e4ae964400eadec15666469d4fce Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sat, 16 Dec 2023 15:35:02 +0000 Subject: [PATCH] Preliminary lemmas --- LeanAPAP.lean | 7 + .../Mathlib/Algebra/BigOperators/Expect.lean | 120 ++++++++++++++---- .../Mathlib/Algebra/BigOperators/Order.lean | 59 +++++---- .../Mathlib/Algebra/BigOperators/Ring.lean | 10 ++ .../Mathlib/Algebra/Order/Field/Basic.lean | 10 ++ LeanAPAP/Mathlib/Data/Complex/Basic.lean | 3 + .../Mathlib/Data/Complex/BigOperators.lean | 10 ++ LeanAPAP/Mathlib/Data/Complex/Order.lean | 33 +++++ LeanAPAP/Mathlib/Data/IsROrC/Basic.lean | 12 +- .../Mathlib/Data/Real/ConjugateExponents.lean | 20 +++ LeanAPAP/Mathlib/Data/Real/Sqrt.lean | 3 +- LeanAPAP/Mathlib/Data/Set/Function.lean | 8 ++ LeanAPAP/Mathlib/Order/BooleanAlgebra.lean | 16 +++ LeanAPAP/Mathlib/Order/Heyting/Basic.lean | 2 +- .../Mathlib/Tactic/Positivity/Finset.lean | 8 +- 15 files changed, 260 insertions(+), 61 deletions(-) create mode 100644 LeanAPAP/Mathlib/Algebra/Order/Field/Basic.lean create mode 100644 LeanAPAP/Mathlib/Data/Complex/BigOperators.lean create mode 100644 LeanAPAP/Mathlib/Data/Complex/Order.lean create mode 100644 LeanAPAP/Mathlib/Data/Real/ConjugateExponents.lean create mode 100644 LeanAPAP/Mathlib/Data/Set/Function.lean create mode 100644 LeanAPAP/Mathlib/Order/BooleanAlgebra.lean diff --git a/LeanAPAP.lean b/LeanAPAP.lean index 287f72d05a..5d57d86304 100644 --- a/LeanAPAP.lean +++ b/LeanAPAP.lean @@ -17,6 +17,7 @@ import LeanAPAP.Mathlib.Algebra.GroupPower.Order import LeanAPAP.Mathlib.Algebra.Group.TypeTags import LeanAPAP.Mathlib.Algebra.ModEq import LeanAPAP.Mathlib.Algebra.Module.Basic +import LeanAPAP.Mathlib.Algebra.Order.Field.Basic import LeanAPAP.Mathlib.Algebra.Order.LatticeGroup import LeanAPAP.Mathlib.Algebra.Order.Ring.Canonical import LeanAPAP.Mathlib.Algebra.Star.Basic @@ -40,7 +41,9 @@ import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Trigonometric.Series import LeanAPAP.Mathlib.Data.Complex.Basic +import LeanAPAP.Mathlib.Data.Complex.BigOperators import LeanAPAP.Mathlib.Data.Complex.Exponential +import LeanAPAP.Mathlib.Data.Complex.Order import LeanAPAP.Mathlib.Data.Finset.Basic import LeanAPAP.Mathlib.Data.Finset.Card import LeanAPAP.Mathlib.Data.Finset.Image @@ -63,9 +66,11 @@ import LeanAPAP.Mathlib.Data.Nat.Parity import LeanAPAP.Mathlib.Data.Pi.Algebra import LeanAPAP.Mathlib.Data.Rat.Order import LeanAPAP.Mathlib.Data.Real.Archimedean +import LeanAPAP.Mathlib.Data.Real.ConjugateExponents import LeanAPAP.Mathlib.Data.Real.ENNReal import LeanAPAP.Mathlib.Data.Real.NNReal import LeanAPAP.Mathlib.Data.Real.Sqrt +import LeanAPAP.Mathlib.Data.Set.Function import LeanAPAP.Mathlib.Data.ZMod.Basic import LeanAPAP.Mathlib.GroupTheory.FiniteAbelian import LeanAPAP.Mathlib.GroupTheory.GroupAction.BigOperators @@ -76,6 +81,7 @@ import LeanAPAP.Mathlib.LinearAlgebra.FiniteDimensional import LeanAPAP.Mathlib.LinearAlgebra.Ray import LeanAPAP.Mathlib.NumberTheory.LegendreSymbol.AddChar.Basic import LeanAPAP.Mathlib.NumberTheory.LegendreSymbol.AddChar.Duality +import LeanAPAP.Mathlib.Order.BooleanAlgebra import LeanAPAP.Mathlib.Order.ConditionallyCompleteLattice.Finset import LeanAPAP.Mathlib.Order.Disjoint import LeanAPAP.Mathlib.Order.Heyting.Basic @@ -91,6 +97,7 @@ import LeanAPAP.Prereqs.Convolution.Norm import LeanAPAP.Prereqs.Convolution.Order import LeanAPAP.Prereqs.Convolution.WithConv import LeanAPAP.Prereqs.Cut +import LeanAPAP.Prereqs.Density import LeanAPAP.Prereqs.DFT import LeanAPAP.Prereqs.Dissociation import LeanAPAP.Prereqs.Energy diff --git a/LeanAPAP/Mathlib/Algebra/BigOperators/Expect.lean b/LeanAPAP/Mathlib/Algebra/BigOperators/Expect.lean index 9ba981a059..b6d8f8e587 100644 --- a/LeanAPAP/Mathlib/Algebra/BigOperators/Expect.lean +++ b/LeanAPAP/Mathlib/Algebra/BigOperators/Expect.lean @@ -3,6 +3,8 @@ import Mathlib.Data.Fintype.Card import Mathlib.Data.IsROrC.Basic import Mathlib.Data.Real.NNReal import LeanAPAP.Mathlib.Algebra.BigOperators.Basic +import LeanAPAP.Mathlib.Algebra.BigOperators.Order +import LeanAPAP.Mathlib.Algebra.Order.Field.Basic import LeanAPAP.Mathlib.Data.Pi.Algebra import LeanAPAP.Mathlib.Tactic.Positivity.Finset @@ -20,27 +22,28 @@ This file defines `Finset.expect`, the average (aka expectation) of a function o * `𝔼 i ∈ s with p i, f i` is notation for `Finset.expect (Finset.filter p s) f`. This is referred to as `expectWith` in lemma names. * `𝔼 (i ∈ s) (j ∈ t), f i j` is notation for `Finset.expect (s ×ˢ t) (fun ⟨i, j⟩ ↦ f i j)`. +-/ -## Naming - -We provide +section +variable {α β : Type*} +/-- Note that the `IsScalarTower α β β` typeclass argument is usually satisfied by `Algebra α β`. -/ +@[to_additive] +lemma smul_div_assoc [DivInvMonoid β] [SMul α β] [IsScalarTower α β β] (r : α) (x y : β) : + r • x / y = r • (x / y) := by simp [div_eq_mul_inv, smul_mul_assoc] + +end open Function open Fintype (card) open scoped NNReal -variable {ι β α 𝕝 : Type*} - -namespace Finset -variable [Semifield α] [Semifield 𝕝] {s : Finset ι} {t : Finset β} {f : ι → α} {g : β → α} +variable {ι κ β α 𝕝 : Type*} /-- Average of a function over a finset. If the finset is empty, this is equal to zero. -/ -def expect (s : Finset ι) (f : ι → α) : α := s.sum f / s.card - -end Finset +def Finset.expect [Semifield α] (s : Finset ι) (f : ι → α) : α := s.sum f / s.card namespace BigOps open Std.ExtendedBinder Lean Meta @@ -96,7 +99,7 @@ open scoped BigOps namespace Finset section Semifield -variable [Semifield α] [Semifield 𝕝] {s : Finset ι} {t : Finset β} {f : ι → α} {g : β → α} +variable [Semifield α] [Semifield 𝕝] {s : Finset ι} {f g : ι → α} {m : β → α} @[simp] lemma expect_empty (f : ι → α) : expect ∅ f = 0 := by simp [expect] @[simp] lemma expect_singleton (f : ι → α) (a : ι) : expect {a} f = f a := by simp [expect] @@ -126,15 +129,19 @@ lemma expect_div (s : Finset ι) (f : ι → α) (a : α) : (𝔼 i ∈ s, f i) lemma expect_univ [Fintype ι] : 𝔼 x, f x = (∑ x, f x) / Fintype.card ι := by rw [expect, card_univ] -lemma expect_congr (f g : ι → α) (h : ∀ x ∈ s, f x = g x) : 𝔼 i ∈ s, f i = 𝔼 i ∈ s, g i := by - rw [expect, expect, sum_congr rfl h] +@[congr] +lemma expect_congr {t : Finset ι} (hst : s = t) (h : ∀ x ∈ t, f x = g x) : + 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by rw [expect, expect, sum_congr hst h, hst] + +lemma expectWith_congr (p : ι → Prop) [DecidablePred p] (h : ∀ x ∈ s, p x → f x = g x) : + 𝔼 i ∈ s with p i, f i = 𝔼 i ∈ s with p i, g i := + expect_congr rfl $ by simpa using h -lemma expectWith_congr (f g : ι → α) (p : ι → Prop) [DecidablePred p] - (h : ∀ x ∈ s, p x → f x = g x) : 𝔼 i ∈ s with p i, f i = 𝔼 i ∈ s with p i, g i := - expect_congr _ _ $ by simpa using h +section bij +variable {t : Finset κ} {g : κ → α} -- TODO: Backport arguments changes to `card_congr` and `prod_bij` -lemma expect_bij (i : ∀ a ∈ s, β) (hi : ∀ a ha, i a ha ∈ t) (h : ∀ a ha, f a = g (i a ha)) +lemma expect_bij (i : ∀ a ∈ s, κ) (hi : ∀ a ha, i a ha ∈ t) (h : ∀ a ha, f a = g (i a ha)) (i_inj : ∀ a₁ ha₁ a₂ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) (i_surj : ∀ b ∈ t, ∃ a ha, i a ha = b) : 𝔼 x ∈ s, f x = 𝔼 x ∈ t, g x := by rw [expect, expect, card_congr i hi (fun _ _ _ _ ↦ i_inj _ _ _ _), @@ -142,12 +149,12 @@ lemma expect_bij (i : ∀ a ∈ s, β) (hi : ∀ a ha, i a ha ∈ t) (h : ∀ a simpa [eq_comm] using i_surj -- TODO: Backport arguments changes to `prod_nbij` -lemma expect_nbij (i : ι → β) (hi : ∀ a ∈ s, i a ∈ t) (h : ∀ a ∈ s, f a = g (i a)) +lemma expect_nbij (i : ι → κ) (hi : ∀ a ∈ s, i a ∈ t) (h : ∀ a ∈ s, f a = g (i a)) (i_inj : (s : Set ι).InjOn i) (i_surj : (s : Set ι).SurjOn i t) : 𝔼 x ∈ s, f x = 𝔼 x ∈ t, g x := expect_bij (fun a _ ↦ i a) hi h i_inj $ by simpa [Set.SurjOn, Set.subset_def] using i_surj -lemma expect_bij' (i : ∀ a ∈ s, β) (hi : ∀ a ha, i a ha ∈ t) (h : ∀ a ha, f a = g (i a ha)) +lemma expect_bij' (i : ∀ a ∈ s, κ) (hi : ∀ a ha, i a ha ∈ t) (h : ∀ a ha, f a = g (i a ha)) (j : ∀ a ∈ t, ι) (hj : ∀ a ha, j a ha ∈ s) (left_inv : ∀ a ha, j (i a ha) (hi a ha) = a) (right_inv : ∀ a ha, i (j a ha) (hj a ha) = a) : 𝔼 x ∈ s, f x = 𝔼 x ∈ t, g x := by rw [expect, expect, sum_bij' i hi h j hj left_inv right_inv, card_congr i hi] @@ -157,16 +164,18 @@ lemma expect_bij' (i : ∀ a ∈ s, β) (hi : ∀ a ha, i a ha ∈ t) (h : ∀ a intro b hb exact ⟨j b hb, hj _ _, right_inv _ _⟩ -lemma expect_nbij' (i : ι → β) (hi : ∀ a ∈ s, i a ∈ t) (h : ∀ a ∈ s, f a = g (i a)) (j : β → ι) +lemma expect_nbij' (i : ι → κ) (hi : ∀ a ∈ s, i a ∈ t) (h : ∀ a ∈ s, f a = g (i a)) (j : κ → ι) (hj : ∀ a ∈ t, j a ∈ s) (left_inv : ∀ a ∈ s, j (i a) = a) (right_inv : ∀ a ∈ t, i (j a) = a) : 𝔼 x ∈ s, f x = 𝔼 x ∈ t, g x := expect_bij' (fun a _ ↦ i a) hi h (fun b _ ↦ j b) hj left_inv right_inv -lemma expect_product' (f : ι → β → α) : 𝔼 x ∈ s ×ˢ t, f x.1 x.2 = 𝔼 x ∈ s, 𝔼 y ∈ t, f x y := by +lemma expect_product' (f : ι → κ → α) : 𝔼 x ∈ s ×ˢ t, f x.1 x.2 = 𝔼 x ∈ s, 𝔼 y ∈ t, f x y := by simp only [expect, expect, card_product, sum_product', ←sum_div, div_div, mul_comm s.card, Nat.cast_mul] -lemma map_expect {F : Type*} [RingHomClass F α 𝕝] (g : F) (f : ι → α) (s : Finset ι) : +end bij + +lemma _root_.map_expect {F : Type*} [RingHomClass F α 𝕝] (g : F) (f : ι → α) (s : Finset ι) : g (𝔼 x ∈ s, f x) = 𝔼 x ∈ s, g (f x) := by simp only [expect, map_div₀, map_natCast, map_sum] variable [CharZero α] @@ -206,6 +215,10 @@ lemma expect_indicate_eq' [Fintype ι] [Nonempty ι] [DecidableEq ι] (f : ι 𝔼 i, ite (i = x) (Fintype.card ι : α) 0 * f i = f x := by simp_rw [@eq_comm _ _ x, expect_indicate_eq] +lemma smul_expect {G : Type*} [DistribSMul G α] [IsScalarTower G α α] (a : G) + (s : Finset ι) (f : ι → α) : a • 𝔼 i ∈ s, f i = 𝔼 i ∈ s, a • f i := by + simp only [expect, ← smul_div_assoc, smul_sum] + end Semifield section Field @@ -215,6 +228,10 @@ lemma expect_sub_distrib (s : Finset ι) (f g : ι → α) : 𝔼 i ∈ s, (f i - g i) = 𝔼 i ∈ s, f i - 𝔼 i ∈ s, g i := by rw [expect, expect, expect, sum_sub_distrib, sub_div] +@[simp] +lemma expect_neg_distrib (s : Finset ι) (f : ι → α) : 𝔼 i ∈ s, -f i = -𝔼 i ∈ s, f i := by + simp [expect, neg_div] + variable [Fintype ι] def balance (f : ι → α) : ι → α := f - Function.const _ (𝔼 y, f y) @@ -265,13 +282,51 @@ lemma expect_nonneg (hf : ∀ i ∈ s, 0 ≤ f i) : 0 ≤ 𝔼 i ∈ s, f i := lemma expect_pos (hf : ∀ i ∈ s, 0 < f i) (hs : s.Nonempty) : 0 < 𝔼 i ∈ s, f i := div_pos (sum_pos hf hs) $ by positivity +lemma expect_eq_zero_iff_of_nonneg (hs : s.Nonempty) (hf : ∀ i ∈ s, 0 ≤ f i) : + 𝔼 i ∈ s, f i = 0 ↔ ∀ i ∈ s, f i = 0 := by + simp [expect, sum_eq_zero_iff_of_nonneg hf, hs.ne_empty] + +lemma expect_eq_zero_iff_of_nonpos (hs : s.Nonempty) (hf : ∀ i ∈ s, f i ≤ 0) : + 𝔼 i ∈ s, f i = 0 ↔ ∀ i ∈ s, f i = 0 := by + simp [expect, sum_eq_zero_iff_of_nonpos hf, hs.ne_empty] + +-- TODO: Contribute back better docstring to `le_prod_of_submultiplicative` +/-- If `m` is a subadditive function (`m (x * y) ≤ f x * f y`, `f 1 = 1`), and `f i`, +`i ∈ s`, is a finite family of elements, then `f (𝔼 i in s, g i) ≤ 𝔼 i in s, f (g i)`. -/ +lemma le_expect_of_subadditive [LinearOrderedSemifield κ] (m : α → κ) (h_zero : m 0 = 0) + (h_add : ∀ a b, m (a + b) ≤ m a + m b) (h_div : ∀ a (n : ℕ), m (a / n) = m a / n) + (s : Finset ι) (f : ι → α) : m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i) := by + simp only [expect, h_div] + exact div_le_div_of_nonneg_right (le_sum_of_subadditive _ h_zero h_add _ _) $ by positivity + end LinearOrderedSemifield + +section LinearOrderedField +variable [LinearOrderedField α] {s : Finset ι} {f g : ι → α} + +lemma abs_expect_le_expect_abs (s : Finset ι) (f : ι → α) : + |𝔼 i ∈ s, f i| ≤ 𝔼 i ∈ s, |f i| := + le_expect_of_subadditive _ abs_zero abs_add (by simp [abs_div]) _ _ + +end LinearOrderedField end Finset +namespace algebraMap +variable {R A : Type*} [Semifield R] [Semifield A] [Algebra R A] + +@[simp, norm_cast] +lemma coe_expect (s : Finset ι) (a : ι → R) : 𝔼 i ∈ s, a i = 𝔼 i ∈ s, (a i : A) := + map_expect (algebraMap R A) a s + +end algebraMap + open Finset namespace Fintype -variable {κ : Type*} [Fintype ι] [Fintype κ] [Semifield α] +variable {κ : Type*} [Fintype ι] [Fintype κ] + +section Semifield +variable [Semifield α] /-- `Fintype.expect_bijective` is a variant of `Finset.expect_bij` that accepts `Function.Bijective`. @@ -290,6 +345,21 @@ lemma expect_equiv (e : ι ≃ κ) (f : ι → α) (g : κ → α) (h : ∀ x, f 𝔼 i, f i = 𝔼 i, g i := expect_bijective _ e.bijective f g h +@[simp] lemma expect_const [Nonempty ι] [CharZero α] (a : α) : 𝔼 _i : ι, a = a := + Finset.expect_const univ_nonempty _ + +end Semifield + +section LinearOrderedSemifield +variable [LinearOrderedSemifield α] [Nonempty ι] {f : ι → α} + +lemma expect_eq_zero_iff_of_nonneg (hf : 0 ≤ f) : 𝔼 i, f i = 0 ↔ f = 0 := by + simp [expect, sum_eq_zero_iff_of_nonneg hf, univ_nonempty.ne_empty] + +lemma expect_eq_zero_iff_of_nonpos (hf : f ≤ 0) : 𝔼 i, f i = 0 ↔ f = 0 := by + simp [expect, sum_eq_zero_iff_of_nonpos hf, univ_nonempty.ne_empty] + +end LinearOrderedSemifield end Fintype namespace IsROrC @@ -314,13 +384,13 @@ def evalFinsetExpect : PositivityExt where eval {u α} zα pα e := do | ~q(@Finset.expect $ι _ $instα $s $f) => let (lhs, _, (rhs : Q($α))) ← lambdaMetaTelescope f let so : Option Q(Finset.Nonempty $s) ← do -- TODO: It doesn't complain if we make a typo? - try { + try let _fi ← synthInstanceQ q(Fintype $ι) let _no ← synthInstanceQ q(Nonempty $ι) match s with | ~q(@univ _ $fi) => pure (some q(Finset.univ_nonempty (α := $ι))) | _ => pure none - } catch _ => do + catch _ => do let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none pure (some (.fvar fv)) match ← core zα pα rhs, so with diff --git a/LeanAPAP/Mathlib/Algebra/BigOperators/Order.lean b/LeanAPAP/Mathlib/Algebra/BigOperators/Order.lean index 77d788fdf7..b59d2c7e11 100644 --- a/LeanAPAP/Mathlib/Algebra/BigOperators/Order.lean +++ b/LeanAPAP/Mathlib/Algebra/BigOperators/Order.lean @@ -3,27 +3,6 @@ import Mathlib.Algebra.BigOperators.Ring open scoped BigOperators -namespace Finset -variable {α 𝕜 : Type*} [LinearOrderedCommRing 𝕜] - -lemma sum_mul_sq_le_sq_mul_sq (s : Finset α) (f g : α → 𝕜) : - (∑ i in s, f i * g i) ^ 2 ≤ (∑ i in s, f i ^ 2) * ∑ i in s, g i ^ 2 := by - have h : 0 ≤ ∑ i in s, (f i * ∑ j in s, g j ^ 2 - g i * ∑ j in s, f j * g j) ^ 2 := - sum_nonneg fun i _ ↦ sq_nonneg _ - simp_rw [sub_sq, sum_add_distrib, Finset.sum_sub_distrib, mul_pow, mul_assoc, ←mul_sum, ← - sum_mul, mul_left_comm, ←mul_assoc, ←sum_mul, mul_right_comm, ←sq, mul_comm, sub_add, - two_mul, add_sub_cancel, sq (∑ j in s, g j ^ 2), ←mul_assoc, ←mul_sub_right_distrib] at h - obtain h' | h' := (sum_nonneg fun i _ ↦ sq_nonneg (g i)).eq_or_lt - · have h'' : ∀ i ∈ s, g i = 0 := fun i hi ↦ by - simpa using (sum_eq_zero_iff_of_nonneg fun i _ ↦ sq_nonneg (g i)).1 h'.symm i hi - rw [←h', sum_congr rfl (show ∀ i ∈ s, f i * g i = 0 from fun i hi ↦ by simp [h'' i hi])] - simp - · rw [←sub_nonneg] - exact nonneg_of_mul_nonneg_left h h' - -end Finset - - namespace Mathlib.Meta.Positivity open Qq Lean Meta Finset @@ -33,13 +12,13 @@ def evalFinsetSum : PositivityExt where eval {u α} zα pα e := do | ~q(@Finset.sum _ $ι $instα $s $f) => let (lhs, _, (rhs : Q($α))) ← lambdaMetaTelescope f let so : Option Q(Finset.Nonempty $s) ← do -- TODO: It doesn't complain if we make a typo? - try { + try let _fi ← synthInstanceQ q(Fintype $ι) let _no ← synthInstanceQ q(Nonempty $ι) match s with | ~q(@univ _ $fi) => pure (some q(Finset.univ_nonempty (α := $ι))) | _ => pure none - } catch _ => do + catch _ => do let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none pure (some (.fvar fv)) match ← core zα pα rhs, so with @@ -63,3 +42,37 @@ example (n : ℕ) (a : ℕ → ℤ) : 0 < ∑ j : Fin (n + 1), (a j^2 + 1) := by example (a : ℕ → ℤ) : 0 < ∑ j in ({1} : Finset ℕ), (a j^2 + 1) := by have : Finset.Nonempty {1} := singleton_nonempty 1 positivity + +end Mathlib.Meta.Positivity + +namespace Finset + +open Function +open scoped BigOperators + +variable {ι N : Type*} [OrderedCommMonoid N] {f g : ι → N} {s t : Finset ι} + +@[to_additive sum_eq_zero_iff_of_nonpos] +lemma prod_eq_one_iff_of_le_one'' : (∀ i ∈ s, f i ≤ 1) → ((∏ i in s, f i) = 1 ↔ ∀ i ∈ s, f i = 1) := + @prod_eq_one_iff_of_one_le' _ Nᵒᵈ _ _ _ + +end Finset + +namespace Finset +variable {α 𝕜 : Type*} [LinearOrderedCommRing 𝕜] + +lemma sum_mul_sq_le_sq_mul_sq (s : Finset α) (f g : α → 𝕜) : + (∑ i in s, f i * g i) ^ 2 ≤ (∑ i in s, f i ^ 2) * ∑ i in s, g i ^ 2 := by + have h : 0 ≤ ∑ i in s, (f i * ∑ j in s, g j ^ 2 - g i * ∑ j in s, f j * g j) ^ 2 := by positivity + simp_rw [sub_sq, sum_add_distrib, Finset.sum_sub_distrib, mul_pow, mul_assoc, ←mul_sum, ← + sum_mul, mul_left_comm, ←mul_assoc, ←sum_mul, mul_right_comm, ←sq, mul_comm, sub_add, + two_mul, add_sub_cancel, sq (∑ j in s, g j ^ 2), ←mul_assoc, ←mul_sub_right_distrib] at h + obtain h' | h' := (sum_nonneg fun i _ ↦ sq_nonneg (g i)).eq_or_lt + · have h'' : ∀ i ∈ s, g i = 0 := fun i hi ↦ by + simpa using (sum_eq_zero_iff_of_nonneg fun i _ ↦ sq_nonneg (g i)).1 h'.symm i hi + rw [←h', sum_congr rfl (show ∀ i ∈ s, f i * g i = 0 from fun i hi ↦ by simp [h'' i hi])] + simp + · rw [←sub_nonneg] + exact nonneg_of_mul_nonneg_left h h' + +end Finset diff --git a/LeanAPAP/Mathlib/Algebra/BigOperators/Ring.lean b/LeanAPAP/Mathlib/Algebra/BigOperators/Ring.lean index 3f9c9e11e0..ce9df42561 100644 --- a/LeanAPAP/Mathlib/Algebra/BigOperators/Ring.lean +++ b/LeanAPAP/Mathlib/Algebra/BigOperators/Ring.lean @@ -58,6 +58,16 @@ lemma sum_mul_sum {ι₁ : Type*} {ι₂ : Type*} [Fintype ι₁] [Fintype ι₂ end Fintype +namespace Fintype +variable {α β : Type*} [CommSemiring β] [DecidableEq α] [Fintype α] +open Finset +open scoped BigOperators + +lemma prod_add (f g : α → β) : ∏ a, (f a + g a) = ∑ t, (∏ a in t, f a) * ∏ a in tᶜ, g a := by + simpa [compl_eq_univ_sdiff] using Finset.prod_add f g univ + +end Fintype + open Finset namespace Nat diff --git a/LeanAPAP/Mathlib/Algebra/Order/Field/Basic.lean b/LeanAPAP/Mathlib/Algebra/Order/Field/Basic.lean new file mode 100644 index 0000000000..fd5e3acca7 --- /dev/null +++ b/LeanAPAP/Mathlib/Algebra/Order/Field/Basic.lean @@ -0,0 +1,10 @@ +import Mathlib.Algebra.Order.Field.Basic + +/-! +### TODO + +Replace in mathlib +-/ + +alias div_le_div_of_pos_left := div_le_div_of_le_left +alias div_le_div_of_nonneg_right := div_le_div_of_le_of_nonneg diff --git a/LeanAPAP/Mathlib/Data/Complex/Basic.lean b/LeanAPAP/Mathlib/Data/Complex/Basic.lean index 7418108809..4df003bc77 100644 --- a/LeanAPAP/Mathlib/Data/Complex/Basic.lean +++ b/LeanAPAP/Mathlib/Data/Complex/Basic.lean @@ -12,4 +12,7 @@ attribute [simp] I_ne_zero @[norm_cast] lemma ofReal'_nsmul (n : ℕ) (r : ℝ) : ofReal' (n • r) = n • ofReal' r := by simp +lemma re_mul_ofReal (z : ℂ) (r : ℝ) : (z * r).re = z.re * r := by simp [ofReal'] +lemma im_mul_ofReal (z : ℂ) (r : ℝ) : (z * r).im = z.im * r := by simp [ofReal'] + end Complex diff --git a/LeanAPAP/Mathlib/Data/Complex/BigOperators.lean b/LeanAPAP/Mathlib/Data/Complex/BigOperators.lean new file mode 100644 index 0000000000..211b3a6f79 --- /dev/null +++ b/LeanAPAP/Mathlib/Data/Complex/BigOperators.lean @@ -0,0 +1,10 @@ +import Mathlib.Data.Complex.BigOperators +import LeanAPAP.Mathlib.Algebra.BigOperators.Expect + +open scoped BigOps + +namespace Complex +variable {α : Type*} (s : Finset α) + +@[simp, norm_cast] +lemma ofReal_expect (f : α → ℝ) : 𝔼 i ∈ s, f i = 𝔼 i ∈ s, (f i : ℂ) := map_expect ofReal _ _ diff --git a/LeanAPAP/Mathlib/Data/Complex/Order.lean b/LeanAPAP/Mathlib/Data/Complex/Order.lean new file mode 100644 index 0000000000..cc42457abc --- /dev/null +++ b/LeanAPAP/Mathlib/Data/Complex/Order.lean @@ -0,0 +1,33 @@ +import Mathlib.Data.Complex.Order + +namespace Mathlib.Meta.Positivity +open Lean Meta Qq Complex +open scoped ComplexOrder + +private alias ⟨_, ofReal_pos⟩ := zero_lt_real +private alias ⟨_, ofReal_nonneg⟩ := zero_le_real +private alias ⟨_, ofReal_ne_zero_of_ne_zero⟩ := ofReal_ne_zero + +/-- Extension for the `positivity` tactic: `Complex.ofReal` is positive/nonnegative/nonzero if its +input is. -/ +@[positivity Complex.ofReal' _] +def evalComplexOfReal : PositivityExt where eval {u α} _ _ e := do + let zα : Q(Zero ℝ) := q(inferInstance) + let pα : Q(PartialOrder ℝ) := q(inferInstance) + if let 0 := u then -- lean4#3060 means we can't combine this with the match below + match α, e with + | ~q(ℂ), ~q(Complex.ofReal' $a) => + assumeInstancesCommute + match ← core zα pα a with + | .positive pa => return .positive q(ofReal_pos $pa) + | .nonnegative pa => return .nonnegative q(ofReal_nonneg $pa) + | .nonzero pa => return .nonzero q(ofReal_ne_zero_of_ne_zero $pa) + | _ => return .none + | _, _ => throwError "not Complex.ofReal'" + else throwError "not Complex.ofReal'" + +example (x : ℝ) (hx : 0 < x) : 0 < (x : ℂ) := by positivity +example (x : ℝ) (hx : 0 ≤ x) : 0 ≤ (x : ℂ) := by positivity +example (x : ℝ) (hx : x ≠ 0) : (x : ℂ) ≠ 0 := by positivity + +end Mathlib.Meta.Positivity diff --git a/LeanAPAP/Mathlib/Data/IsROrC/Basic.lean b/LeanAPAP/Mathlib/Data/IsROrC/Basic.lean index ca1eabed69..409e70cf2f 100644 --- a/LeanAPAP/Mathlib/Data/IsROrC/Basic.lean +++ b/LeanAPAP/Mathlib/Data/IsROrC/Basic.lean @@ -5,8 +5,13 @@ open scoped ComplexConjugate namespace IsROrC variable {K : Type*} [IsROrC K] {x : K} +lemma mul_conj' (x : K) : x * conj x = (‖x‖ : K) ^ 2 := by rw [mul_conj, normSq_eq_def']; norm_cast +lemma conj_mul' (x : K) : conj x * x = (‖x‖ : K) ^ 2 := by rw [conj_mul, normSq_eq_def']; norm_cast + lemma inv_eq_conj (hx : ‖x‖ = 1) : x⁻¹ = conj x := - inv_eq_of_mul_eq_one_left $ by simp_rw [conj_mul, normSq_eq_def', hx, one_pow, algebraMap.coe_one] + inv_eq_of_mul_eq_one_left $ by simp_rw [conj_mul', hx, algebraMap.coe_one, one_pow] + +@[simp] lemma conj_div (x y : K) : conj (x / y) = conj x / conj y := map_div' conj conj_inv _ _ --TODO: Do we rather want the map as an explicit definition? lemma exists_norm_eq_mul_self (x : K) : ∃ c, ‖c‖ = 1 ∧ ↑‖x‖ = c * x := by @@ -19,9 +24,4 @@ lemma exists_norm_mul_eq_self (x : K) : ∃ c, ‖c‖ = 1 ∧ c * ‖x‖ = x : · exact ⟨1, by simp⟩ · exact ⟨x / ‖x‖, by simp [norm_ne_zero_iff.2, hx]⟩ -lemma mul_conj' (x : K) : x * conj x = (‖x‖ : K) ^ 2 := by rw [mul_conj, normSq_eq_def']; norm_cast -lemma conj_mul' (x : K) : conj x * x = (‖x‖ : K) ^ 2 := by rw [conj_mul, normSq_eq_def']; norm_cast - -@[simp] lemma conj_div (x y : K) : conj (x / y) = conj x / conj y := map_div' conj conj_inv _ _ - end IsROrC diff --git a/LeanAPAP/Mathlib/Data/Real/ConjugateExponents.lean b/LeanAPAP/Mathlib/Data/Real/ConjugateExponents.lean new file mode 100644 index 0000000000..bda003721c --- /dev/null +++ b/LeanAPAP/Mathlib/Data/Real/ConjugateExponents.lean @@ -0,0 +1,20 @@ +import Mathlib.Data.Real.ConjugateExponents + +/-! +## TODO + +Change everything to using `x⁻¹` instead of `1 / x`. +-/ + +namespace Real.IsConjugateExponent +variable {p q : ℝ} (h : p.IsConjugateExponent q) + +lemma inv_add_inv_conj' : p⁻¹ + q⁻¹ = 1 := by simpa only [one_div] using h.inv_add_inv_conj + +lemma inv_add_inv_conj_nnreal' : p.toNNReal⁻¹ + q.toNNReal⁻¹ = 1 := by + simpa only [one_div] using h.inv_add_inv_conj_nnreal + +lemma inv_add_inv_conj_ennreal' : (ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = 1 := by + simpa only [one_div] using h.inv_add_inv_conj_ennreal + +end Real.IsConjugateExponent diff --git a/LeanAPAP/Mathlib/Data/Real/Sqrt.lean b/LeanAPAP/Mathlib/Data/Real/Sqrt.lean index 31edc264ce..3e0464c2ee 100644 --- a/LeanAPAP/Mathlib/Data/Real/Sqrt.lean +++ b/LeanAPAP/Mathlib/Data/Real/Sqrt.lean @@ -24,8 +24,7 @@ namespace Finset lemma cauchy_schwarz_sqrt {α : Type*} (s : Finset α) (f g : α → ℝ) : ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ 2).sqrt * (∑ i in s, g i ^ 2).sqrt := - (Real.le_sqrt_of_sq_le $ sum_mul_sq_le_sq_mul_sq _ _ _).trans_eq $ - Real.sqrt_mul (sum_nonneg fun _ _ ↦ sq_nonneg _) _ + (Real.le_sqrt_of_sq_le $ sum_mul_sq_le_sq_mul_sq _ _ _).trans_eq $ Real.sqrt_mul (by positivity) _ end Finset diff --git a/LeanAPAP/Mathlib/Data/Set/Function.lean b/LeanAPAP/Mathlib/Data/Set/Function.lean new file mode 100644 index 0000000000..d3bf6e03d4 --- /dev/null +++ b/LeanAPAP/Mathlib/Data/Set/Function.lean @@ -0,0 +1,8 @@ +import Mathlib.Data.Set.Function + +namespace Set +variable {α β : Type*} {f : α → β} {s : Set α} {a b : α} + +@[simp] lemma injOn_pair : InjOn f {a, b} ↔ f a = f b → a = b := by unfold InjOn; aesop + +end Set diff --git a/LeanAPAP/Mathlib/Order/BooleanAlgebra.lean b/LeanAPAP/Mathlib/Order/BooleanAlgebra.lean new file mode 100644 index 0000000000..8420511048 --- /dev/null +++ b/LeanAPAP/Mathlib/Order/BooleanAlgebra.lean @@ -0,0 +1,16 @@ +import Mathlib.Order.BooleanAlgebra +import LeanAPAP.Mathlib.Order.Disjoint + +section +variable {α : Type*} [GeneralizedBooleanAlgebra α] {a b : α} + +@[simp] lemma sdiff_eq_right : a \ b = b ↔ a = ⊥ ∧ b = ⊥ := by + refine ⟨fun h ↦ ?_, ?_⟩ + · obtain ⟨h, rfl⟩ := disjoint_sdiff_self_left.eq_iff.1 h + simpa using h + · rintro ⟨rfl, rfl⟩ + exact bot_sdiff + +lemma sdiff_ne_right : a \ b ≠ b ↔ a ≠ ⊥ ∨ b ≠ ⊥ := sdiff_eq_right.not.trans not_and_or + +end diff --git a/LeanAPAP/Mathlib/Order/Heyting/Basic.lean b/LeanAPAP/Mathlib/Order/Heyting/Basic.lean index addfe95319..f5ccc4fcc3 100644 --- a/LeanAPAP/Mathlib/Order/Heyting/Basic.lean +++ b/LeanAPAP/Mathlib/Order/Heyting/Basic.lean @@ -1,4 +1,4 @@ -import Mathlib.Order.BooleanAlgebra +import Mathlib.Order.Heyting.Basic section variable {α : Type*} [GeneralizedHeytingAlgebra α] {a b : α} diff --git a/LeanAPAP/Mathlib/Tactic/Positivity/Finset.lean b/LeanAPAP/Mathlib/Tactic/Positivity/Finset.lean index cbc288dffb..46dbd11d85 100644 --- a/LeanAPAP/Mathlib/Tactic/Positivity/Finset.lean +++ b/LeanAPAP/Mathlib/Tactic/Positivity/Finset.lean @@ -10,14 +10,14 @@ def evalFinsetCard : PositivityExt where eval {u α} _ _ e := do if let 0 := u then -- lean4#3060 means we can't combine this with the match below match α, e with | ~q(ℕ), ~q(@Finset.card $β $s) => - let so : Option Q(Finset.Nonempty $s) ← do -- TODO: if I make a typo it doesn't complain? - try { + let so : Option Q(Finset.Nonempty $s) ← do -- TODO: It doesn't complain if we make a typo? + try let _fi ← synthInstanceQ q(Fintype $β) let _no ← synthInstanceQ q(Nonempty $β) match s with | ~q(@univ _ $fi) => pure (some q(Finset.univ_nonempty (α := $β))) - | _ => pure none } - catch _e => do + | _ => pure none + catch _ => do let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none pure (some (.fvar fv)) assumeInstancesCommute