From e4cd901c11ccb37e4de528327a2d89c228f807fb Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Fri, 3 Jul 2026 21:50:39 -0700 Subject: [PATCH 1/3] refactor: golf Space norm and distance-bound proofs Golf proof bodies in Space/Norm/Basic and Space/IsDistBounded: term-mode collapses, Tendsto composition in place of manual rpow juggling, and anonymous-constructor witnesses. Statements unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3 --- Physlib/SpaceAndTime/Space/IsDistBounded.lean | 766 +++++------------- Physlib/SpaceAndTime/Space/Norm/Basic.lean | 712 +++++----------- 2 files changed, 415 insertions(+), 1063 deletions(-) diff --git a/Physlib/SpaceAndTime/Space/IsDistBounded.lean b/Physlib/SpaceAndTime/Space/IsDistBounded.lean index 30963783f..194d5594f 100644 --- a/Physlib/SpaceAndTime/Space/IsDistBounded.lean +++ b/Physlib/SpaceAndTime/Space/IsDistBounded.lean @@ -125,20 +125,14 @@ lemma aeStronglyMeasurable_fderiv_schwartzMap_smul {d : ℕ} {f : Space d → F} @[fun_prop] lemma aeStronglyMeasurable_inv_pow {d r : ℕ} {f : Space d → F} (hf : IsDistBounded f) : - AEStronglyMeasurable (fun x => ‖((1 + ‖x‖) ^ r)⁻¹‖ • f x) := by - apply AEStronglyMeasurable.smul - · apply AEMeasurable.aestronglyMeasurable - fun_prop - · fun_prop + AEStronglyMeasurable (fun x => ‖((1 + ‖x‖) ^ r)⁻¹‖ • f x) := + AEStronglyMeasurable.smul (AEMeasurable.aestronglyMeasurable (by fun_prop)) (by fun_prop) @[fun_prop] lemma aeStronglyMeasurable_time_schwartzMap_smul {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) (η : 𝓢(Time × Space d, ℝ)) : - AEStronglyMeasurable (fun x => η x • f x.2) := by - apply AEStronglyMeasurable.smul - · fun_prop - · apply MeasureTheory.AEStronglyMeasurable.comp_snd - fun_prop + AEStronglyMeasurable (fun x => η x • f x.2) := + AEStronglyMeasurable.smul (by fun_prop) (AEStronglyMeasurable.comp_snd (by fun_prop)) /-! @@ -158,20 +152,13 @@ lemma integrable_space {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) · fun_prop · filter_upwards with x rw [norm_smul] - apply le_trans (mul_le_mul_of_nonneg_left (bound x) (norm_nonneg (η x))) - apply le_of_eq + refine (mul_le_mul_of_nonneg_left (bound x) (norm_nonneg (η x))).trans (le_of_eq ?_) simp only [Real.norm_eq_abs] rw [Finset.abs_sum_of_nonneg (fun i _ => mul_nonneg (c_nonneg i) (by positivity)), Finset.mul_sum] ring_nf - · apply MeasureTheory.integrable_finsetSum - intro i _ - apply Integrable.const_mul - specialize h2 (p i) (p_bound i) (g i) η - rw [← MeasureTheory.integrable_norm_iff] at h2 - simpa using h2 - apply AEMeasurable.aestronglyMeasurable - fun_prop + · refine MeasureTheory.integrable_finsetSum _ fun i _ => Integrable.const_mul ?_ _ + simpa using (h2 (p i) (p_bound i) (g i) η).norm /- Reducing the problem to `Integrable (fun x : Space d => η x * ‖x‖ ^ p)` -/ suffices h0 : ∀ (p : ℤ) (hp : - (d - 1 : ℕ) ≤ p) (η : 𝓢(Space d, ℝ)), Integrable (fun x : Space d => η x * ‖x‖ ^ p) volume by @@ -192,27 +179,22 @@ lemma integrable_space {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) positivity /- Proving `Integrable (fun x : Space d => η x * ‖x + c‖ ^ p)` -/ intro p hp η - have h1 : AEStronglyMeasurable (fun (x : Space d) => ‖x‖ ^ p) volume := - AEMeasurable.aestronglyMeasurable <| by fun_prop - rw [← MeasureTheory.integrable_norm_iff (by fun_prop)] + rw [← MeasureTheory.integrable_norm_iff (AEMeasurable.aestronglyMeasurable (by fun_prop))] simp only [norm_mul, norm_zpow, norm_norm] match d with | 0 => simp only [Real.norm_eq_abs, Integrable.of_finite] | d + 1 => by_cases hp' : p = 0 · subst hp' - simp only [zpow_zero, mul_one] - exact Integrable.norm η.integrable + simpa using η.integrable.norm suffices h1 : Integrable (fun x => ‖η x‖ * ‖x‖ ^ (p + d)) (radialAngularMeasure (d := (d + 1))) by rw [integrable_radialAngularMeasure_iff] at h1 convert h1 using 1 funext x - have hx : 0 ≤ ‖x‖ := norm_nonneg x - generalize ‖x‖ = r at * + generalize ‖x‖ = r simp only [Real.norm_eq_abs, add_tsub_cancel_right, one_div, smul_eq_mul] - trans |η x| * ((r ^ d)⁻¹ *r ^ (p + d)); swap - · ring - congr + rw [mul_left_comm] + congr 1 by_cases hr : r = 0 · subst hr simp [zero_pow_eq, zero_zpow_eq, hp'] @@ -222,12 +204,7 @@ lemma integrable_space {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) convert integrable_pow_mul_iteratedFDeriv radialAngularMeasure η (p + d).toNat 0 using 1 funext x simp only [Real.norm_eq_abs, norm_iteratedFDeriv_zero] - rw [mul_comm] - congr 1 - rw [← zpow_natCast] - congr - refine Int.eq_natCast_toNat.mpr ?_ - omega + rw [mul_comm, ← zpow_natCast, Int.toNat_of_nonneg (by omega)] @[fun_prop] lemma integrable_space_mul {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) @@ -237,14 +214,14 @@ lemma integrable_space_mul {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f @[fun_prop] lemma integrable_space_fderiv {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) (η : 𝓢(Space d, ℝ)) (y : Space d) : - Integrable (fun x : Space d => fderiv ℝ η x y • f x) volume := by - exact hf.integrable_space (LineDeriv.lineDerivOpCLM ℝ _ y η) + Integrable (fun x : Space d => fderiv ℝ η x y • f x) volume := + hf.integrable_space (LineDeriv.lineDerivOpCLM ℝ _ y η) @[fun_prop] lemma integrable_space_fderiv_mul {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) (η : 𝓢(Space d, ℝ)) (y : Space d) : - Integrable (fun x : Space d => fderiv ℝ η x y * f x) volume := by - exact hf.integrable_space (LineDeriv.lineDerivOpCLM ℝ _ y η) + Integrable (fun x : Space d => fderiv ℝ η x y * f x) volume := + hf.integrable_space (LineDeriv.lineDerivOpCLM ℝ _ y η) /-! @@ -275,12 +252,10 @@ instance {D1 : Type} [NormedAddCommGroup D1] [MeasurableSpace D1] rw [abs_of_nonneg (by positivity)] simp only [Real.rpow_neg_natCast, zpow_neg, zpow_natCast] apply mul_le_mul _ _ (by positivity) (by positivity) - · refine inv_anti₀ (by positivity) (pow_le_pow_left₀ (by positivity) ?_ rt1) - rcases x - simp - · refine inv_anti₀ (by positivity) (pow_le_pow_left₀ (by positivity) ?_ rt2) - rcases x - simp + · exact inv_anti₀ (by positivity) + (pow_le_pow_left₀ (by positivity) (by simpa using norm_fst_le x) rt1) + · exact inv_anti₀ (by positivity) + (pow_le_pow_left₀ (by positivity) (by simpa using norm_snd_le x) rt2) @[fun_prop] lemma integrable_time_space {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) @@ -294,20 +269,13 @@ lemma integrable_time_space {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) · fun_prop · filter_upwards with x rw [norm_smul] - apply le_trans (mul_le_mul_of_nonneg_left (bound x.2) (norm_nonneg (η x))) - apply le_of_eq + refine (mul_le_mul_of_nonneg_left (bound x.2) (norm_nonneg (η x))).trans (le_of_eq ?_) simp only [Real.norm_eq_abs] rw [Finset.abs_sum_of_nonneg (fun i _ => mul_nonneg (c_nonneg i) (by positivity)), Finset.mul_sum] ring_nf - · apply MeasureTheory.integrable_finsetSum - intro i _ - apply Integrable.const_mul - specialize h2 (p i) (p_bound i) (g i) η - rw [← MeasureTheory.integrable_norm_iff] at h2 - simpa using h2 - apply AEMeasurable.aestronglyMeasurable - fun_prop + · refine MeasureTheory.integrable_finsetSum _ fun i _ => Integrable.const_mul ?_ _ + simpa using (h2 (p i) (p_bound i) (g i) η).norm /- Reducing the problem to `Integrable (fun x : Space d => η x * ‖x‖ ^ p)` -/ suffices h0 : ∀ (p : ℤ) (hp : - (d - 1 : ℕ) ≤ p) (η : 𝓢(Time × Space d, ℝ)), Integrable (fun x : Time × Space d => η x * ‖x.2‖ ^ p) volume by @@ -375,22 +343,12 @@ lemma integrable_time_space {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) · simp · fun_prop apply Integrable.mono' (integrable_pow_mul_iteratedFDeriv _ η (p + (d - 1 : ℕ)).toNat 0) - · apply AEMeasurable.aestronglyMeasurable - fun_prop + (AEMeasurable.aestronglyMeasurable (by fun_prop)) filter_upwards with x simp only [Real.norm_eq_abs, norm_iteratedFDeriv_zero] - rw [mul_comm, ← zpow_natCast, abs_of_nonneg (by positivity)] - apply mul_le_mul _ (by rfl) (by positivity) (by positivity) - rw [zpow_natCast] - trans ‖x.2‖ ^ ((p + (d - 1 : ℕ)).toNat : ℤ) - · apply le_of_eq - congr - refine Int.eq_natCast_toNat.mpr (by omega) - rw [zpow_natCast] - ring_nf - apply pow_le_pow_left₀ (by positivity) _ (p + (d - 1 : ℕ)).toNat - rcases x - simp + rw [abs_of_nonneg (by positivity), mul_comm, ← zpow_natCast, Int.toNat_of_nonneg (by omega)] + exact mul_le_mul_of_nonneg_right + (zpow_le_zpow_left₀ (by omega) (norm_nonneg _) (norm_snd_le x)) (abs_nonneg _) /-! @@ -409,29 +367,23 @@ lemma integrable_mul_inv_pow {d : ℕ} | 0 => simp at bound; simp [bound] | n + 1 => let pMax := Finset.max' (Finset.image p Finset.univ) (by simp) - have pMax_max (i : Fin n.succ) : p i ≤ pMax := by - simp [pMax] - apply Finset.le_max' - simp + have pMax_max (i : Fin n.succ) : p i ≤ pMax := + Finset.le_max' _ _ (Finset.mem_image_of_mem p (Finset.mem_univ i)) obtain ⟨r, hr⟩ := h0 pMax use r apply Integrable.mono (g := fun x => ∑ i, (c i * (‖((1 + ‖x‖) ^ r)⁻¹‖ * ‖x + g i‖ ^ p i))) _ · fun_prop · filter_upwards with x rw [norm_smul] - apply le_trans (mul_le_mul_of_nonneg_left (bound x) (by positivity)) - apply le_of_eq + refine (mul_le_mul_of_nonneg_left (bound x) (by positivity)).trans (le_of_eq ?_) simp only [norm_inv, norm_pow, Real.norm_eq_abs, abs_abs] rw [Finset.abs_sum_of_nonneg (fun i _ => mul_nonneg (c_nonneg i) (by positivity)), Finset.mul_sum] ring_nf - · apply MeasureTheory.integrable_finsetSum - intro i _ - apply Integrable.const_mul - apply (hr (p i) (p_bound i) (g i) (pMax_max i)).mono - · fun_prop - · filter_upwards with x - simp + · refine MeasureTheory.integrable_finsetSum _ fun i _ => Integrable.const_mul ?_ _ + refine (hr (p i) (p_bound i) (g i) (pMax_max i)).mono (by fun_prop) ?_ + filter_upwards with x + simp match d with | 0 => simp | d + 1 => @@ -440,19 +392,18 @@ lemma integrable_mul_inv_pow {d : ℕ} intro pMax use (pMax + d).toNat + (radialAngularMeasure (d := d + 1)).integrablePower intro p hp c p_le - apply (h0 (p + d).toNat c).mono - · fun_prop - · filter_upwards with x - simp only [norm_inv, norm_pow, Real.norm_eq_abs, norm_mul, abs_abs, norm_zpow, - Int.ofNat_toNat] - rw [mul_comm] - refine mul_le_mul ?_ ?_ (by positivity) (by positivity) - · rw [max_eq_left (by omega)] + refine (h0 (p + d).toNat c).mono (by fun_prop) ?_ + filter_upwards with x + simp only [norm_inv, norm_pow, Real.norm_eq_abs, norm_mul, abs_abs, norm_zpow, + Int.ofNat_toNat] + rw [mul_comm] + refine mul_le_mul ?_ ?_ (by positivity) (by positivity) + · rw [max_eq_left (by omega)] + simp + · refine inv_pow_le_inv_pow_of_le ?_ ?_ + · rw [abs_of_nonneg (by positivity)] simp - · refine inv_pow_le_inv_pow_of_le ?_ ?_ - · rw [abs_of_nonneg (by positivity)] - simp - · simp_all + · simp_all let m := (radialAngularMeasure (d := (d + 1))).integrablePower suffices h0 : ∀ (q : ℕ) (c : Space (d + 1)), Integrable (fun x => ‖x‖ ^ (q - d : ℤ) * ‖((1 + ‖x - c‖) ^ (q + m))⁻¹‖) volume by @@ -465,12 +416,8 @@ lemma integrable_mul_inv_pow {d : ℕ} intro q v specialize h0 q v rw [integrable_radialAngularMeasure_iff] at h0 - apply Integrable.congr h0 - rw [Filter.eventuallyEq_iff_exists_mem] - use {0}ᶜ - constructor - · rw [compl_mem_ae_iff, measure_singleton] - intro x hx + refine h0.congr (Filter.eventuallyEq_of_mem (compl_mem_ae_iff.mpr (measure_singleton 0)) + fun x hx => ?_) simp [← mul_assoc] left rw [zpow_sub₀ (by simpa using hx), zpow_natCast, zpow_natCast] @@ -480,54 +427,20 @@ lemma integrable_mul_inv_pow {d : ℕ} ‖((1 + ‖x - v‖) ^ (q + m))⁻¹‖ = ((1 + ‖x - v‖) ^ (q + m))⁻¹ := by simp only [norm_inv, norm_pow, Real.norm_eq_abs, inv_inj] rw [abs_of_nonneg (by positivity)] - apply integrable_of_le_of_pow_mul_le (C₁ := 1) (C₂ :=2 ^ (q + m - 1) * (‖v‖ ^ (q + m) + 1)) - · simp - intro x - refine inv_le_one_of_one_le₀ ?_ - rw [abs_of_nonneg (by positivity)] - refine one_le_pow₀ ?_ - simp + apply integrable_of_le_of_pow_mul_le (C₁ := 1) (C₂ := (1 + ‖v‖) ^ (q + m)) + · intro x + rw [hr1] + exact inv_le_one_of_one_le₀ (one_le_pow₀ (by simp)) · intro x rw [hr1] refine mul_inv_le_of_le_mul₀ ?_ (by positivity) ?_ · positivity - change ‖x‖^ (q + m) ≤ _ - by_cases hzero : m = 0 ∧ q = 0 - · rcases hzero with ⟨hm, hq⟩ - generalize hm : m = m' at * - subst hm hq - rw [pow_zero, pow_zero] - simp - trans (‖v‖ + ‖x - v‖) ^ (q + m) - · rw [pow_le_pow_iff_left₀] - · apply norm_le_norm_add_norm_sub' - · positivity - · positivity - simp only [ne_eq, Nat.add_eq_zero_iff, not_and] - intro hq - omega - apply (add_pow_le _ _ _).trans - trans 2 ^ (q + m - 1) * (‖v‖ ^ (q + m) + ‖x - v‖ ^ (q + m)) + (2 ^ (q + m - 1) - + 2 ^ (q + m - 1) * ‖v‖ ^ (q + m) * ‖x - v‖ ^ (q + m)) - · simp - positivity - trans (2 ^ (q + m - 1) * (‖v‖ ^ (q + m) + 1)) * (1 + ‖x - v‖ ^ (q + m)) - · apply le_of_eq - ring - refine mul_le_mul_of_nonneg (by rfl) ?_ ?_ ?_ - · trans 1 ^ (q + m) + ‖x - v‖ ^ (q + m) - · simp - apply pow_add_pow_le - · simp - · positivity - · simp - omega - · positivity - · positivity - · positivity - · positivity - · refine Measurable.aestronglyMeasurable ?_ - fun_prop + change ‖x‖ ^ (q + m) ≤ _ + calc ‖x‖ ^ (q + m) ≤ ((1 + ‖v‖) * (1 + ‖x - v‖)) ^ (q + m) := by + refine pow_le_pow_left₀ (norm_nonneg x) ?_ _ + nlinarith [norm_le_norm_add_norm_sub' x v, norm_nonneg (x - v), norm_nonneg v] + _ = (1 + ‖v‖) ^ (q + m) * (1 + ‖x - v‖) ^ (q + m) := mul_pow _ _ _ + · exact Measurable.aestronglyMeasurable (by fun_prop) /-! @@ -546,13 +459,8 @@ lemma integral_mul_schwartzMap_bounded {d : ℕ} {f : Space d → F} (hf : IsDis refine integral_mono_of_nonneg ?_ ?_ ?_ · filter_upwards with x positivity - · apply Integrable.mul_const - apply Integrable.const_mul - apply Integrable.congr' hr - · apply AEStronglyMeasurable.mul - · fun_prop - · apply AEMeasurable.aestronglyMeasurable - fun_prop + · refine (Integrable.congr' hr (AEStronglyMeasurable.mul (by fun_prop) + (AEMeasurable.aestronglyMeasurable (by fun_prop))) ?_).const_mul _ |>.mul_const _ filter_upwards with x simp [norm_smul, mul_comm] · filter_upwards with x @@ -565,7 +473,7 @@ lemma integral_mul_schwartzMap_bounded {d : ℕ} {f : Space d → F} (hf : IsDis apply mul_le_mul_of_nonneg ?_ (by rfl) (by positivity) (by positivity) have h0 := one_add_le_sup_seminorm_apply (𝕜 := ℝ) (m := (r, 0)) (k := r) (n := 0) le_rfl le_rfl η x - rw [Lean.Grind.Field.IsOrdered.le_mul_inv_iff_mul_le _ _ (by positivity)] + rw [le_mul_inv_iff₀ (by positivity)] convert! h0 using 1 simp only [norm_iteratedFDeriv_zero, Real.norm_eq_abs] ring_nf @@ -584,11 +492,8 @@ variable (𝕜 : Type) {E F F' : Type} [RCLike 𝕜] [NormedAddCommGroup E] [Nor [NormedAddCommGroup F'] [NormedSpace ℝ F'] @[fun_prop] -lemma zero {d} : IsDistBounded (0 : Space d → F) := by - apply And.intro - · fun_prop - use 1, fun _ => 0, fun _ => 0, fun _ => 0 - simp +lemma zero {d} : IsDistBounded (0 : Space d → F) := + ⟨by fun_prop, 1, fun _ => 0, fun _ => 0, fun _ => 0, by simp⟩ /-! @@ -598,35 +503,20 @@ lemma zero {d} : IsDistBounded (0 : Space d → F) := by @[fun_prop] lemma add {d : ℕ} {f g : Space d → F} (hf : IsDistBounded f) (hg : IsDistBounded g) : IsDistBounded (f + g) := by - apply And.intro - · fun_prop rcases hf with ⟨hae1, ⟨n1, c1, g1, p1, c1_nonneg, p1_bound, bound1⟩⟩ rcases hg with ⟨hae2, ⟨n2, c2, g2, p2, c2_nonneg, p2_bound, bound2⟩⟩ - refine ⟨n1 + n2, Fin.append c1 c2, Fin.append g1 g2, Fin.append p1 p2, ?_, ?_, ?_⟩ + refine ⟨by fun_prop, n1 + n2, Fin.append c1 c2, Fin.append g1 g2, Fin.append p1 p2, ?_, ?_, ?_⟩ · intro i - obtain ⟨i, rfl⟩ := finSumFinEquiv.surjective i - match i with - | .inl i => - simp only [finSumFinEquiv_apply_left, Fin.append_left, ge_iff_le] - exact c1_nonneg i - | .inr i => - simp only [finSumFinEquiv_apply_right, Fin.append_right, ge_iff_le] - exact c2_nonneg i + induction i using Fin.addCases with + | left i => simpa using c1_nonneg i + | right i => simpa using c2_nonneg i · intro i - obtain ⟨i, rfl⟩ := finSumFinEquiv.surjective i - match i with - | .inl i => - simp only [finSumFinEquiv_apply_left, Fin.append_left, ge_iff_le] - exact p1_bound i - | .inr i => - simp only [finSumFinEquiv_apply_right, Fin.append_right, ge_iff_le] - exact p2_bound i + induction i using Fin.addCases with + | left i => simpa using p1_bound i + | right i => simpa using p2_bound i · intro x - apply (norm_add_le _ _).trans - apply (add_le_add (bound1 x) (bound2 x)).trans - apply le_of_eq - rw [← finSumFinEquiv.sum_comp] - simp + refine ((norm_add_le _ _).trans (add_le_add (bound1 x) (bound2 x))).trans_eq ?_ + simp [Fin.sum_univ_add] @[fun_prop] lemma fun_add {d : ℕ} {f g : Space d → F} @@ -641,20 +531,15 @@ lemma fun_add {d : ℕ} {f g : Space d → F} lemma sum {ι : Type*} {s : Finset ι} {d : ℕ} {f : ι → Space d → F} (hf : ∀ i ∈ s, IsDistBounded (f i)) : IsDistBounded (∑ i ∈ s, f i) := by classical - induction' s using Finset.induction with i s hi ih - · simp - fun_prop - rw [Finset.sum_insert] - apply IsDistBounded.add - · exact hf i (s.mem_insert_self i) - · exact ih (fun j hj => hf j (s.mem_insert_of_mem hj)) - exact hi + induction s using Finset.induction with + | empty => simpa using zero + | insert i s hi ih => + rw [Finset.sum_insert hi] + exact (hf i (s.mem_insert_self i)).add (ih fun j hj => hf j (s.mem_insert_of_mem hj)) lemma sum_fun {ι : Type*} {s : Finset ι} {d : ℕ} {f : ι → Space d → F} - (hf : ∀ i ∈ s, IsDistBounded (f i)) : IsDistBounded (fun x => ∑ i ∈ s, f i x) := by - convert sum hf using 1 - funext x - simp + (hf : ∀ i ∈ s, IsDistBounded (f i)) : IsDistBounded (fun x => ∑ i ∈ s, f i x) := + Finset.sum_fn s f ▸ sum hf /-! @@ -666,27 +551,15 @@ lemma sum_fun {ι : Type*} {s : Finset ι} {d : ℕ} {f : ι → Space d → F} lemma const_smul {d : ℕ} [NormedSpace ℝ F] {f : Space d → F} (hf : IsDistBounded f) (c : ℝ) : IsDistBounded (c • f) := by rcases hf with ⟨hae1, ⟨n1, c1, g1, p1, c1_nonneg, p1_bound, bound1⟩⟩ - apply And.intro - · fun_prop - refine ⟨n1, ‖c‖ • c1, g1, p1, ?_, p1_bound, ?_⟩ - · intro i - simp only [Real.norm_eq_abs, Pi.smul_apply, smul_eq_mul] - have hi := c1_nonneg i - positivity - · intro x - simp [norm_smul] - conv_rhs => enter [2, x]; rw [mul_assoc] - rw [← Finset.mul_sum] - refine mul_le_mul (by rfl) (bound1 x) ?_ ?_ - · exact norm_nonneg (f x) - · exact abs_nonneg c + refine ⟨by fun_prop, n1, ‖c‖ • c1, g1, p1, + fun i => mul_nonneg (norm_nonneg c) (c1_nonneg i), p1_bound, fun x => ?_⟩ + simp only [Pi.smul_apply, norm_smul, smul_eq_mul, mul_assoc, ← Finset.mul_sum] + exact mul_le_mul_of_nonneg_left (bound1 x) (norm_nonneg c) @[fun_prop] lemma neg {d : ℕ} [NormedSpace ℝ F] {f : Space d → F} (hf : IsDistBounded f) : IsDistBounded (fun x => - f x) := by - convert hf.const_smul (-1) using 1 - funext x - simp + simpa [Pi.neg_def] using hf.const_smul (-1) @[fun_prop] lemma const_fun_smul {d : ℕ} [NormedSpace ℝ F] {f : Space d → F} @@ -701,9 +574,7 @@ lemma const_mul_fun {d : ℕ} lemma mul_const_fun {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) (c : ℝ) : IsDistBounded (fun x => f x * c) := by - convert hf.const_smul c using 2 - simp only [Pi.smul_apply, smul_eq_mul] - ring + simpa [Pi.smul_def, mul_comm] using hf.const_smul c /-! @@ -716,28 +587,13 @@ lemma pi_comp {d n : ℕ} {f : Space d → EuclideanSpace ℝ (Fin n)} (hf : IsDistBounded f) (j : Fin n) : IsDistBounded (fun x => f x j) := by rcases hf with ⟨hae1, ⟨n1, c1, g1, p1, c1_nonneg, p1_bound, bound1⟩⟩ - apply And.intro - · fun_prop - refine ⟨n1, c1, g1, p1, c1_nonneg, p1_bound, ?_⟩ - intro x - apply le_trans ?_ (bound1 x) - simp only [Real.norm_eq_abs] - rw [@PiLp.norm_eq_of_L2] - refine Real.abs_le_sqrt ?_ - trans ∑ i ∈ {j}, ‖(f x) i‖ ^ 2 - · simp - apply Finset.sum_le_univ_sum_of_nonneg - intro y - exact sq_nonneg ‖f x y‖ + exact ⟨by fun_prop, n1, c1, g1, p1, c1_nonneg, p1_bound, + fun x => (PiLp.norm_apply_le (f x) j).trans (bound1 x)⟩ lemma vector_component {d n : ℕ} {f : Space d → Lorentz.Vector n} (hf : IsDistBounded f) (j : Fin 1 ⊕ Fin n) : IsDistBounded (fun x => f x j) := by rcases hf with ⟨hae1, ⟨n1, c1, g1, p1, c1_nonneg, p1_bound, bound1⟩⟩ - apply And.intro - · fun_prop - refine ⟨n1, c1, g1, p1, c1_nonneg, p1_bound, ?_⟩ - intro x - apply le_trans ?_ (bound1 x) + refine ⟨by fun_prop, n1, c1, g1, p1, c1_nonneg, p1_bound, fun x => le_trans ?_ (bound1 x)⟩ simp [Real.norm_eq_abs] /-! @@ -750,20 +606,10 @@ lemma comp_add_right {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) (c : Space d) : IsDistBounded (fun x => f (x + c)) := by rcases hf with ⟨hae1, ⟨n1, c1, g1, p1, c1_nonneg, p1_bound, bound1⟩⟩ - apply And.intro - · simp - apply AEStronglyMeasurable.comp_measurable - · rw [Measure.IsAddRightInvariant.map_add_right_eq_self] - fun_prop - · fun_prop - refine ⟨n1, c1, fun i => g1 i + c, p1, c1_nonneg, p1_bound, ?_⟩ - intro x - apply (bound1 (x + c)).trans - apply le_of_eq - congr 1 - funext x - congr 3 - module + refine ⟨hae1.comp_measurePreserving (measurePreserving_add_right volume c), + n1, c1, fun i => g1 i + c, p1, c1_nonneg, p1_bound, fun x => ?_⟩ + refine (bound1 (x + c)).trans_eq (Finset.sum_congr rfl fun i _ => ?_) + rw [add_right_comm, add_assoc] lemma comp_sub_right {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) (c : Space d) : @@ -781,12 +627,7 @@ lemma congr {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) (hae : AEStronglyMeasurable g) (hfg : ∀ x, ‖g x‖ = ‖f x‖) : IsDistBounded g := by rcases hf with ⟨hae1, ⟨n1, c1, g1, p1, c1_nonneg, p1_bound, bound1⟩⟩ - apply And.intro - · exact hae - refine ⟨n1, c1, g1, p1, c1_nonneg, p1_bound, ?_⟩ - intro x - rw [hfg x] - exact bound1 x + exact ⟨hae, n1, c1, g1, p1, c1_nonneg, p1_bound, fun x => (hfg x).le.trans (bound1 x)⟩ /-! @@ -800,11 +641,7 @@ lemma mono {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) (hae : AEStronglyMeasurable g) (hfg : ∀ x, ‖g x‖ ≤ ‖f x‖) : IsDistBounded g := by rcases hf with ⟨hae1, ⟨n1, c1, g1, p1, c1_nonneg, p1_bound, bound1⟩⟩ - apply And.intro - · exact hae - refine ⟨n1, c1, g1, p1, c1_nonneg, p1_bound, ?_⟩ - intro x - exact (hfg x).trans (bound1 x) + exact ⟨hae, n1, c1, g1, p1, c1_nonneg, p1_bound, fun x => (hfg x).trans (bound1 x)⟩ /-! @@ -819,21 +656,11 @@ lemma inner_left {d n : ℕ} (hf : IsDistBounded f) (y : EuclideanSpace ℝ (Fin n)) : IsDistBounded (fun x => ⟪f x, y⟫_ℝ) := by rcases hf with ⟨hae1, ⟨n1, c1, g1, p1, c1_nonneg, p1_bound, bound1⟩⟩ - apply And.intro - · fun_prop - refine ⟨n1, fun i => ‖y‖ * c1 i, g1, p1, ?_, p1_bound, ?_⟩ - · intro i - simp only - have hi := c1_nonneg i - positivity - · intro x - apply (norm_inner_le_norm (f x) y).trans - rw [mul_comm] - conv_rhs => enter [2, i]; rw [mul_assoc] - rw [← Finset.mul_sum] - refine mul_le_mul (by rfl) (bound1 x) ?_ ?_ - · exact norm_nonneg (f x) - · exact norm_nonneg y + refine ⟨by fun_prop, n1, fun i => ‖y‖ * c1 i, g1, p1, + fun i => mul_nonneg (norm_nonneg y) (c1_nonneg i), p1_bound, fun x => ?_⟩ + simp only [mul_assoc, ← Finset.mul_sum] + exact ((norm_inner_le_norm (f x) y).trans_eq (mul_comm _ _)).trans + (mul_le_mul_of_nonneg_left (bound1 x) (norm_nonneg y)) /-! @@ -842,12 +669,8 @@ lemma inner_left {d n : ℕ} @[fun_prop] lemma smul_const {d : ℕ} [NormedSpace ℝ F] {c : Space d → ℝ} - (hc : IsDistBounded c) (f : F) : IsDistBounded (fun x => c x • f) := by - apply IsDistBounded.congr (f := fun x => (c x) * ‖f‖) - · fun_prop - · fun_prop - · intro x - simp [norm_smul] + (hc : IsDistBounded c) (f : F) : IsDistBounded (fun x => c x • f) := + (hc.mul_const_fun ‖f‖).congr (by fun_prop) fun x => by simp [norm_smul] /-! ## E. Specific functions that are `IsDistBounded` @@ -862,11 +685,8 @@ lemma smul_const {d : ℕ} [NormedSpace ℝ F] {c : Space d → ℝ} @[fun_prop] lemma const {d : ℕ} (f : F) : - IsDistBounded (d := d) (fun _ : Space d => f) := by - apply And.intro - · fun_prop - use 1, fun _ => ‖f‖, fun _ => 0, fun _ => 0 - simp + IsDistBounded (d := d) (fun _ : Space d => f) := + ⟨by fun_prop, 1, fun _ => ‖f‖, fun _ => 0, fun _ => 0, by simp⟩ /-! @@ -876,37 +696,21 @@ lemma const {d : ℕ} (f : F) : @[fun_prop] lemma pow {d : ℕ} (n : ℤ) (hn : - (d - 1 : ℕ) ≤ n) : - IsDistBounded (d := d) (fun x => ‖x‖ ^ n) := by - apply And.intro - · apply AEMeasurable.aestronglyMeasurable - fun_prop - refine ⟨1, fun _ => 1, fun _ => 0, fun _ => n, ?_, ?_, ?_⟩ - · simp - · simp - exact hn - · intro x - simp + IsDistBounded (d := d) (fun x => ‖x‖ ^ n) := + ⟨AEMeasurable.aestronglyMeasurable (by fun_prop), 1, fun _ => 1, fun _ => 0, fun _ => n, + fun _ => zero_le_one, fun _ => hn, fun x => by simp⟩ @[fun_prop] lemma pow_shift {d : ℕ} (n : ℤ) (g : Space d) (hn : - (d - 1 : ℕ) ≤ n) : - IsDistBounded (d := d) (fun x => ‖x - g‖ ^ n) := by - apply And.intro - · apply AEMeasurable.aestronglyMeasurable - fun_prop - refine ⟨1, fun _ => 1, fun _ => (- g), fun _ => n, ?_, ?_, ?_⟩ - · simp - · simp - exact hn - · intro x - simp [sub_eq_add_neg] + IsDistBounded (d := d) (fun x => ‖x - g‖ ^ n) := + ⟨AEMeasurable.aestronglyMeasurable (by fun_prop), 1, fun _ => 1, fun _ => - g, fun _ => n, + fun _ => zero_le_one, fun _ => hn, fun x => by simp [sub_eq_add_neg]⟩ @[fun_prop] lemma inv_shift {d : ℕ} (g : Space d) (hd : 2 ≤ d := by omega) : IsDistBounded (d := d) (fun x => ‖x - g‖⁻¹) := by - convert IsDistBounded.pow_shift (d := d) (-1) g (by omega) using 1 - ext1 x - simp + simpa using IsDistBounded.pow_shift (d := d) (-1) g (by omega) @[fun_prop] lemma nat_pow {d : ℕ} (n : ℕ) : IsDistBounded (d := d) (fun x => ‖x‖ ^ n) := IsDistBounded.pow (d := d) (n : ℤ) (by omega) @@ -914,12 +718,8 @@ lemma nat_pow {d : ℕ} (n : ℕ) : @[fun_prop] lemma norm_add_nat_pow {d : ℕ} (n : ℕ) (a : ℝ) : IsDistBounded (d := d) (fun x => (‖x‖ + a) ^ n) := by - conv => - enter [1, x] - rw [add_pow] - apply IsDistBounded.sum_fun - intro i _ - fun_prop + simp only [add_pow] + exact sum_fun fun i _ => by fun_prop @[fun_prop] lemma norm_add_pos_nat_zpow {d : ℕ} (n : ℤ) (a : ℝ) (ha : 0 < a) : @@ -927,131 +727,81 @@ lemma norm_add_pos_nat_zpow {d : ℕ} (n : ℤ) (a : ℝ) (ha : 0 < a) : match n with | Int.ofNat n => fun_prop | Int.negSucc n => - apply IsDistBounded.mono (f := fun x => (a ^ ((n + 1)))⁻¹) - · fun_prop - · apply AEMeasurable.aestronglyMeasurable - fun_prop - · intro x - simp only [zpow_negSucc, norm_inv, norm_pow, Real.norm_eq_abs] - refine inv_anti₀ (by positivity) ?_ - refine (pow_le_pow_iff_left₀ (by positivity) (by positivity) (by simp)).mpr ?_ - rw [abs_of_nonneg (by positivity), abs_of_nonneg (by positivity)] - simp + refine IsDistBounded.mono (f := fun x => (a ^ ((n + 1)))⁻¹) (by fun_prop) + (AEMeasurable.aestronglyMeasurable (by fun_prop)) fun x => ?_ + simp only [zpow_negSucc, norm_inv, norm_pow, Real.norm_eq_abs, abs_of_nonneg ha.le, + abs_of_nonneg (show (0:ℝ) ≤ ‖x‖ + a by positivity)] + exact inv_anti₀ (by positivity) (pow_le_pow_left₀ ha.le (by simp) _) @[fun_prop] lemma nat_pow_shift {d : ℕ} (n : ℕ) (g : Space d) : - IsDistBounded (d := d) (fun x => ‖x - g‖ ^ n) := by - exact IsDistBounded.pow_shift (d := d) (n : ℤ) g (by omega) + IsDistBounded (d := d) (fun x => ‖x - g‖ ^ n) := + IsDistBounded.pow_shift (d := d) (n : ℤ) g (by omega) @[fun_prop] lemma norm_sub {d : ℕ} (g : Space d) : IsDistBounded (d := d) (fun x => ‖x - g‖) := by - convert IsDistBounded.nat_pow_shift (d := d) 1 g using 1 - ext1 x - simp + simpa using IsDistBounded.nat_pow_shift (d := d) 1 g @[fun_prop] lemma norm_add {d : ℕ} (g : Space d) : IsDistBounded (d := d) (fun x => ‖x + g‖) := by - convert IsDistBounded.nat_pow_shift (d := d) 1 (- g) using 1 - ext1 x - simp + simpa using IsDistBounded.nat_pow_shift (d := d) 1 (- g) @[fun_prop] lemma inv {d : ℕ} (hd: 2 ≤ d := by omega): IsDistBounded (d := d) (fun x => ‖x‖⁻¹) := by - convert IsDistBounded.pow (d := d) (-1) (by omega) using 1 - ext1 x - simp + simpa using IsDistBounded.pow (d := d) (-1) (by omega) @[fun_prop] lemma norm {d : ℕ} : IsDistBounded (d := d) (fun x => ‖x‖) := by - convert IsDistBounded.nat_pow (d := d) 1 using 1 - ext1 x - simp + simpa using IsDistBounded.nat_pow (d := d) 1 @[fun_prop] lemma log_norm {d : ℕ} (hd : 2 ≤ d := by omega) : IsDistBounded (d := d) (fun x => Real.log ‖x‖) := by - apply IsDistBounded.mono (f := fun x => ‖x‖⁻¹ + ‖x‖) - · fun_prop - · apply AEMeasurable.aestronglyMeasurable - fun_prop - · intro x - simp only [Real.norm_eq_abs] - conv_rhs => rw [abs_of_nonneg (by positivity)] - have h1 := Real.neg_inv_le_log (x := ‖x‖) (by positivity) - have h2 := Real.log_le_rpow_div (x := ‖x‖) (by positivity) (ε := 1) (by positivity) - simp_all - rw [abs_le'] - generalize Real.log ‖x‖ = r at * - apply And.intro - · apply h2.trans - simp - · rw [neg_le] - apply le_trans _ h1 - simp + refine IsDistBounded.mono (f := fun x => ‖x‖⁻¹ + ‖x‖) (by fun_prop) + (AEMeasurable.aestronglyMeasurable (by fun_prop)) fun x => ?_ + have h1 := Real.neg_inv_le_log (x := ‖x‖) (norm_nonneg x) + have h2 := Real.log_le_rpow_div (x := ‖x‖) (norm_nonneg x) one_pos + simp only [Real.rpow_one, div_one] at h2 + rw [Real.norm_eq_abs, Real.norm_eq_abs, + abs_of_nonneg (show (0:ℝ) ≤ ‖x‖⁻¹ + ‖x‖ by positivity), abs_le'] + constructor + · exact h2.trans (by simp) + · linarith [norm_nonneg x] lemma zpow_smul_self {d : ℕ} (n : ℤ) (hn : - (d - 1 : ℕ) - 1 ≤ n) : IsDistBounded (d := d) (fun x => ‖x‖ ^ n • x) := by by_cases hzero : n = -1 - · apply IsDistBounded.mono (f := fun x => (1 : ℝ)) - · fun_prop - · apply AEMeasurable.aestronglyMeasurable - fun_prop - · intro x - simp [norm_smul] - subst hzero - simp only [Int.reduceNeg, zpow_neg, zpow_one] - by_cases hx : x = 0 - · subst hx - simp - rw [inv_mul_cancel₀] - simpa using hx - apply IsDistBounded.congr (f := fun x => ‖x‖ ^ (n + 1)) - · apply pow - omega - · apply AEMeasurable.aestronglyMeasurable - fun_prop - · intro x - by_cases hx : x = 0 - · subst hx - simp only [norm_zero, smul_zero, norm_zpow] - rw [@zero_zpow_eq] - rw [if_neg] - omega - · simp [norm_smul] - rw [zpow_add₀] - simp only [zpow_one] - ring_nf - simpa using hx + · subst hzero + refine IsDistBounded.mono (f := fun x => (1 : ℝ)) (by fun_prop) + (AEMeasurable.aestronglyMeasurable (by fun_prop)) fun x => ?_ + simpa [norm_smul, inv_mul_eq_div] using div_self_le_one ‖x‖ + refine IsDistBounded.congr (f := fun x => ‖x‖ ^ (n + 1)) (pow _ (by omega)) + (AEMeasurable.aestronglyMeasurable (by fun_prop)) fun x => ?_ + rcases eq_or_ne x 0 with rfl | hx + · simp [zero_zpow (n + 1) (by omega)] + · simp [norm_smul, zpow_add₀ (norm_ne_zero_iff.mpr hx), mul_comm] lemma zpow_smul_repr_self {d : ℕ} (n : ℤ) (hn : - (d - 1 : ℕ) - 1 ≤ n) : - IsDistBounded (d := d) (fun x => ‖x‖ ^ n • basis.repr x) := by - apply IsDistBounded.congr (f := fun x => ‖x‖ ^ n • x) - · exact zpow_smul_self n hn - · apply AEMeasurable.aestronglyMeasurable - fun_prop - · intro x - simp [norm_smul] + IsDistBounded (d := d) (fun x => ‖x‖ ^ n • basis.repr x) := + (zpow_smul_self n hn).congr (AEMeasurable.aestronglyMeasurable (by fun_prop)) + fun x => by simp [norm_smul] lemma zpow_smul_repr_self_sub {d : ℕ} (n : ℤ) (hn : - (d - 1 : ℕ) - 1 ≤ n) (y : Space d) : - IsDistBounded (d := d) (fun x => ‖x - y‖ ^ n • basis.repr (x - y)) := by - apply (zpow_smul_repr_self n hn).comp_sub_right y + IsDistBounded (d := d) (fun x => ‖x - y‖ ^ n • basis.repr (x - y)) := + (zpow_smul_repr_self n hn).comp_sub_right y lemma inv_pow_smul_self {d : ℕ} (n : ℕ) (hn : - (d - 1 : ℕ) - 1 ≤ (- n : ℤ)) : IsDistBounded (d := d) (fun x => ‖x‖⁻¹ ^ n • x) := by - convert zpow_smul_self (n := - (n : ℤ)) (by omega) using 1 - funext x - simp + simpa using zpow_smul_self (n := - (n : ℤ)) (by omega) lemma inv_pow_smul_repr_self {d : ℕ} (n : ℕ) (hn : - (d - 1 : ℕ) - 1 ≤ (- n : ℤ)) : IsDistBounded (d := d) (fun x => ‖x‖⁻¹ ^ n • basis.repr x) := by - convert zpow_smul_repr_self (n := - (n : ℤ)) (by omega) using 1 - funext x - simp + simpa using zpow_smul_repr_self (n := - (n : ℤ)) (by omega) /-! @@ -1061,31 +811,15 @@ lemma inv_pow_smul_repr_self {d : ℕ} (n : ℕ) (hn : - (d - 1 : ℕ) - 1 ≤ ( lemma norm_smul_nat_pow {d} (p : ℕ) (c : Space d) : IsDistBounded (fun x => ‖x‖ * ‖x + c‖ ^ p) := by - apply IsDistBounded.mono (f := fun x => ‖x‖ * (‖x‖ + ‖c‖) ^ p) - · conv => - enter [1, x] - rw [add_pow] - rw [Finset.mul_sum] - apply IsDistBounded.sum_fun - intro i _ - conv => - enter [1, x] - rw [← mul_assoc, ← mul_assoc] - apply IsDistBounded.mul_const_fun - apply IsDistBounded.mul_const_fun - convert IsDistBounded.nat_pow (n := i + 1) using 1 - funext x - ring - · apply AEMeasurable.aestronglyMeasurable - fun_prop - · intro x - simp [norm_mul, norm_pow, Real.norm_eq_abs] + refine IsDistBounded.mono (f := fun x => ‖x‖ * (‖x‖ + ‖c‖) ^ p) ?_ + (AEMeasurable.aestronglyMeasurable (by fun_prop)) fun x => ?_ + · simp only [add_pow, Finset.mul_sum, ← mul_assoc] + refine IsDistBounded.sum_fun fun i _ => mul_const_fun (mul_const_fun ?_ _) _ + simpa [pow_succ'] using IsDistBounded.nat_pow (d := d) (i + 1) + · simp [norm_mul, norm_pow, Real.norm_eq_abs] rw [abs_of_nonneg (by positivity)] - have h1 : ‖x + c‖ ≤ ‖x‖ + ‖c‖ := norm_add_le x c - have h2 : ‖x + c‖ ^ p ≤ (‖x‖ + ‖c‖) ^ p := by - refine pow_le_pow_left₀ (by positivity) h1 p - apply (mul_le_mul (by rfl) h2 (by positivity) (by positivity)).trans - rfl + gcongr + exact norm_add_le x c lemma norm_smul_zpow {d} (p : ℤ) (c : Space d) (hn : - (d - 1 : ℕ) ≤ p) : IsDistBounded (fun x => ‖x‖ * ‖x + c‖ ^ p) := by @@ -1093,80 +827,48 @@ lemma norm_smul_zpow {d} (p : ℤ) (c : Space d) (hn : - (d - 1 : ℕ) ≤ p) : | Int.ofNat p => exact norm_smul_nat_pow p c | Int.negSucc p => suffices h0 : IsDistBounded (fun x => ‖x - c‖ * (‖x‖ ^ (p + 1))⁻¹) by - convert h0.comp_sub_right (- c) using 1 - funext x - simp + simpa using h0.comp_sub_right (- c) suffices h0 : IsDistBounded (fun x => (‖x‖ + ‖c‖) * (‖x‖ ^ (p + 1))⁻¹) by - apply h0.mono - · fun_prop - · intro x - simp [norm_mul, norm_inv, norm_pow, Real.norm_eq_abs] - rw [abs_of_nonneg (by positivity)] - apply mul_le_mul (norm_sub_le x c) (by rfl) (by positivity) (by positivity) + refine h0.mono (by fun_prop) fun x => ?_ + simp [norm_mul, norm_inv, norm_pow, Real.norm_eq_abs] + rw [abs_of_nonneg (by positivity)] + gcongr + exact norm_sub_le x c suffices h0 : IsDistBounded (fun x => ‖x‖ * (‖x‖ ^ (p + 1))⁻¹ + ‖c‖ * (‖x‖ ^ (p + 1))⁻¹) by - convert h0 using 1 - funext x - ring + simpa [add_mul] using h0 suffices h0 : IsDistBounded (fun x => ‖x‖ * (‖x‖ ^ (p + 1))⁻¹) by - apply h0.add - · apply IsDistBounded.const_mul_fun - exact IsDistBounded.pow (d := d) (n := -(p + 1)) (by grind) + refine h0.add (const_mul_fun ?_ ‖c‖) + exact IsDistBounded.pow (d := d) (n := -(p + 1)) (by grind) by_cases hp : p = 0 · subst hp simp only [zero_add, pow_one] - apply IsDistBounded.mono (f := fun x => (1 : ℝ)) - · fun_prop - · apply AEMeasurable.aestronglyMeasurable - fun_prop - · intro x - simp only [norm_mul, norm_norm, norm_inv, one_mem, CStarRing.norm_of_mem_unitary] - by_cases hx : ‖x‖ ≠ 0 - · rw [mul_inv_cancel₀ (by positivity)] - · simp at hx - subst hx - simp + refine IsDistBounded.mono (f := fun x => (1 : ℝ)) (by fun_prop) + (AEMeasurable.aestronglyMeasurable (by fun_prop)) fun x => ?_ + simpa [← div_eq_mul_inv] using div_self_le_one ‖x‖ convert IsDistBounded.pow (d := d) (n := - p) (by grind) using 1 funext x - trans (‖x‖ ^ p)⁻¹; swap - · rw [@zpow_neg] - simp - by_cases hx : ‖x‖ ≠ 0 - field_simp - ring - simp at hx - subst hx - simp only [norm_zero, ne_eq, Nat.add_eq_zero_iff, one_ne_zero, and_false, not_false_eq_true, - zero_pow, inv_zero, mul_zero, zero_eq_inv] - rw [@zero_pow_eq] - simp [hp] + rw [zpow_neg, zpow_natCast] + rcases eq_or_ne ‖x‖ 0 with hx | hx + · simp [hx, zero_pow hp] + · field_simp + ring @[fun_prop] lemma norm_smul_isDistBounded {d : ℕ} [NormedSpace ℝ F] {f : Space d → F} (hf : IsDistBounded f) : IsDistBounded (fun x => ‖x‖ • f x) := by obtain ⟨hae, ⟨n, c, g, p, c_nonneg, p_bound, bound⟩⟩ := hf - apply IsDistBounded.mono (f := fun x => ‖x‖ * ∑ i, (c i * ‖x + g i‖ ^ (p i))) - · apply IsDistBounded.congr (f := fun x => ∑ i, (c i * (‖x‖ * ‖x + g i‖ ^ (p i)))) - · apply IsDistBounded.sum_fun - intro i _ - exact IsDistBounded.const_mul_fun (norm_smul_zpow (p i) (g i) (p_bound i)) (c i) - · fun_prop - · intro x - congr - rw [Finset.mul_sum] - congr - funext i - ring - · fun_prop - · intro x - simp [_root_.norm_smul] - apply (mul_le_mul (by rfl) (bound x) (by positivity) (by positivity)).trans - rw [abs_of_nonneg] - apply Finset.sum_nonneg - intro i _ - apply mul_nonneg - · exact c_nonneg i - · positivity + refine IsDistBounded.mono (f := fun x => ‖x‖ * ∑ i, (c i * ‖x + g i‖ ^ (p i))) + (IsDistBounded.congr (f := fun x => ∑ i, (c i * (‖x‖ * ‖x + g i‖ ^ (p i)))) + (sum_fun fun i _ => const_mul_fun (norm_smul_zpow (p i) (g i) (p_bound i)) (c i)) + (by fun_prop) fun x => ?_) (by fun_prop) fun x => ?_ + · rw [Finset.mul_sum] + congr 1 + exact Finset.sum_congr rfl fun i _ => mul_left_comm _ _ _ + · have h : (0:ℝ) ≤ ∑ i, c i * ‖x + g i‖ ^ p i := + Finset.sum_nonneg fun i _ => mul_nonneg (c_nonneg i) (by positivity) + simp only [_root_.norm_smul, Real.norm_eq_abs, abs_mul, abs_norm, abs_of_nonneg h] + exact mul_le_mul_of_nonneg_left (bound x) (norm_nonneg x) @[fun_prop] lemma norm_mul_isDistBounded {d : ℕ} {f : Space d → ℝ} @@ -1177,17 +879,12 @@ lemma norm_mul_isDistBounded {d : ℕ} {f : Space d → ℝ} lemma component_smul_isDistBounded {d : ℕ} [NormedSpace ℝ F] {f : Space d → F} (hf : IsDistBounded f) (i : Fin d) : IsDistBounded (fun x => x i • f x) := by - apply IsDistBounded.mono (f := fun x => ‖x‖ • f x) - · fun_prop - · apply AEStronglyMeasurable.smul - · have h1 : AEStronglyMeasurable (fun x => Space.coordCLM i x) := by fun_prop - convert h1 using 1 - funext i - simp [coordCLM_apply, coord_apply] - · fun_prop - · intro x - simp [norm_smul] - exact mul_le_mul (abs_eval_le_norm x i) (by rfl) (by positivity) (by positivity) + refine IsDistBounded.mono (f := fun x => ‖x‖ • f x) (by fun_prop) + (AEStronglyMeasurable.smul ?_ (by fun_prop)) fun x => ?_ + · simpa [coordCLM_apply, coord_apply] using + (by fun_prop : AEStronglyMeasurable (fun x => Space.coordCLM i x)) + · simp [norm_smul] + exact mul_le_mul_of_nonneg_right (abs_eval_le_norm x i) (by positivity) @[fun_prop] lemma component_mul_isDistBounded {d : ℕ} {f : Space d → ℝ} @@ -1197,58 +894,34 @@ lemma component_mul_isDistBounded {d : ℕ} {f : Space d → ℝ} @[fun_prop] lemma isDistBounded_smul_self {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) : IsDistBounded (fun x => f x • x) := by - apply IsDistBounded.congr (f := fun x => ‖x‖ * f x) - · fun_prop - · apply AEStronglyMeasurable.smul - · fun_prop - · fun_prop - · intro x - simp [norm_smul] - ring + refine IsDistBounded.congr (f := fun x => ‖x‖ * f x) (by fun_prop) + (AEStronglyMeasurable.smul (by fun_prop) (by fun_prop)) fun x => ?_ + simp [norm_smul, mul_comm] @[fun_prop] lemma isDistBounded_smul_self_repr {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) : IsDistBounded (fun x => f x • basis.repr x) := by - apply IsDistBounded.congr (f := fun x => ‖x‖ * f x) - · fun_prop - · apply AEStronglyMeasurable.smul - · fun_prop - · fun_prop - · intro x - simp [norm_smul] - ring + refine IsDistBounded.congr (f := fun x => ‖x‖ * f x) (by fun_prop) + (AEStronglyMeasurable.smul (by fun_prop) (by fun_prop)) fun x => ?_ + simp [norm_smul, mul_comm] @[fun_prop] lemma isDistBounded_smul_inner {d : ℕ} [NormedSpace ℝ F] {f : Space d → F} (hf : IsDistBounded f) (y : Space d) : IsDistBounded (fun x => ⟪y, x⟫_ℝ • f x) := by have h1 (x : Space d) : ⟪y, x⟫_ℝ • f x = ∑ i, (y i * x i) • f x := by rw [inner_eq_sum, ← Finset.sum_smul] - conv => - enter [1, x] - rw [h1 x] - apply IsDistBounded.sum_fun - intro i _ - simp [← smul_smul] - refine const_fun_smul ?_ (y i) - fun_prop + simp only [h1, ← smul_smul] + exact sum_fun fun i _ => const_fun_smul (by fun_prop) (y i) lemma isDistBounded_smul_inner_of_smul_norm {d : ℕ} [NormedSpace ℝ F] {f : Space d → F} (hf : IsDistBounded (fun x => ‖x‖ • f x)) (hae : AEStronglyMeasurable f) (y : Space d) : IsDistBounded (fun x => ⟪y, x⟫_ℝ • f x) := by have h1 (x : Space d) : ⟪y, x⟫_ℝ • f x = ∑ i, (y i * x i) • f x := by rw [inner_eq_sum, ← Finset.sum_smul] - conv => - enter [1, x] - rw [h1 x] - apply IsDistBounded.sum_fun - intro i _ - simp [← smul_smul] - refine const_fun_smul ?_ (y i) - apply hf.mono - · fun_prop - · intro x - simp [norm_smul] - exact mul_le_mul_of_nonneg_right (abs_eval_le_norm x i) (by positivity) + simp only [h1, ← smul_smul] + refine sum_fun fun i _ => const_fun_smul (hf.mono (by fun_prop) fun x => ?_) (y i) + simp [norm_smul] + exact mul_le_mul_of_nonneg_right (abs_eval_le_norm x i) (by positivity) @[fun_prop] lemma isDistBounded_mul_inner {d : ℕ} {f : Space d → ℝ} @@ -1257,9 +930,7 @@ lemma isDistBounded_mul_inner {d : ℕ} {f : Space d → ℝ} lemma isDistBounded_mul_inner' {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) (y : Space d) : IsDistBounded (fun x => ⟪x, y⟫_ℝ * f x) := by - convert! hf.isDistBounded_smul_inner y using 2 - rw [real_inner_comm] - simp + simpa only [smul_eq_mul, real_inner_comm y] using hf.isDistBounded_smul_inner y lemma isDistBounded_mul_inner_of_smul_norm {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded (fun x => ‖x‖ * f x)) (hae : AEStronglyMeasurable f) (y : Space d) : @@ -1268,24 +939,17 @@ lemma isDistBounded_mul_inner_of_smul_norm {d : ℕ} {f : Space d → ℝ} @[fun_prop] lemma mul_inner_pow_neg_two {d : ℕ} (y : Space d) (hd : 2 ≤ d := by omega) : IsDistBounded (fun x => ⟪y, x⟫_ℝ * ‖x‖ ^ (- 2 : ℤ)) := by - apply IsDistBounded.mono (f := fun x => (‖y‖ * ‖x‖) * ‖x‖ ^ (- 2 : ℤ)) - · simp [mul_assoc] - apply IsDistBounded.const_mul_fun - apply IsDistBounded.congr (f := fun x => ‖x‖ ^ (- 1 : ℤ)) - · apply IsDistBounded.pow (d := d) (-1) (by omega) - · apply AEMeasurable.aestronglyMeasurable - fun_prop - · intro x - simp only [norm_mul, norm_norm, norm_inv, norm_zpow, Int.reduceNeg, zpow_neg, zpow_one] - by_cases hx : x = 0 - · subst hx - simp - have hx' : ‖x‖ ≠ 0 := by simpa using hx - field_simp - · apply AEMeasurable.aestronglyMeasurable - fun_prop - · intro x - simp + refine IsDistBounded.mono (f := fun x => (‖y‖ * ‖x‖) * ‖x‖ ^ (- 2 : ℤ)) ?_ + (AEMeasurable.aestronglyMeasurable (by fun_prop)) fun x => ?_ + · simp only [mul_assoc] + refine IsDistBounded.const_mul_fun (IsDistBounded.congr (f := fun x => ‖x‖ ^ (- 1 : ℤ)) + (IsDistBounded.pow (d := d) (-1) (by omega)) + (AEMeasurable.aestronglyMeasurable (by fun_prop)) fun x => ?_) ‖y‖ + simp only [norm_mul, norm_norm, norm_inv, norm_zpow, Int.reduceNeg, zpow_neg, zpow_one] + rcases eq_or_ne x 0 with rfl | hx + · simp + · field_simp [norm_ne_zero_iff.mpr hx] + · simp exact mul_le_mul_of_nonneg (abs_real_inner_le_norm y x) (by rfl) (by positivity) (by positivity) end constructors diff --git a/Physlib/SpaceAndTime/Space/Norm/Basic.lean b/Physlib/SpaceAndTime/Space/Norm/Basic.lean index db6c0bd0d..f4efd35aa 100644 --- a/Physlib/SpaceAndTime/Space/Norm/Basic.lean +++ b/Physlib/SpaceAndTime/Space/Norm/Basic.lean @@ -95,10 +95,8 @@ lemma normPowerSeries_eq (n : ℕ) : normPowerSeries (d := d) n = fun x => √(‖x‖ ^ 2 + 1/(n + 1)) := rfl lemma normPowerSeries_eq_rpow {d} (n : ℕ) : - normPowerSeries (d := d) n = fun x => ((‖x‖ ^ 2 + 1/(n + 1))) ^ (1/2 : ℝ) := by - rw [normPowerSeries_eq] - funext x - rw [← Real.sqrt_eq_rpow] + normPowerSeries (d := d) n = fun x => ((‖x‖ ^ 2 + 1/(n + 1))) ^ (1/2 : ℝ) := + funext fun _ => Real.sqrt_eq_rpow _ /-! @@ -109,15 +107,9 @@ lemma normPowerSeries_eq_rpow {d} (n : ℕ) : @[fun_prop] lemma normPowerSeries_differentiable {d} (n : ℕ) : Differentiable ℝ (fun (x : Space d) => normPowerSeries n x) := by - rw [normPowerSeries_eq_rpow] - refine Differentiable.rpow_const ?_ ?_ - · refine (Differentiable.fun_add_iff_right ?_).mpr ?_ - · apply Differentiable.norm_sq ℝ - fun_prop - · fun_prop - · intro x - have h1 : 0 < ‖x‖ ^ 2 + 1 / (↑n + 1) := by positivity - grind + rw [normPowerSeries_eq] + intro x + exact ((differentiable_id.norm_sq ℝ).add_const _).differentiableAt.sqrt (by positivity) /-! @@ -130,25 +122,14 @@ open scoped Topology BigOperators FourierTransform lemma normPowerSeries_tendsto {d} (x : Space d) (hx : x ≠ 0) : Filter.Tendsto (fun n => normPowerSeries n x) Filter.atTop (𝓝 (‖x‖)) := by - conv => enter [1, n]; rw [normPowerSeries_eq_rpow] - simp only [one_div] - have hx_norm : ‖x‖ = (‖x‖ ^ 2 + 0) ^ (1 / 2 : ℝ) := by - rw [← Real.sqrt_eq_rpow] - simp - conv_rhs => rw [hx_norm] - refine Filter.Tendsto.rpow ?_ ?_ ?_ - · apply Filter.Tendsto.add - · exact tendsto_const_nhds - · simpa using tendsto_one_div_add_atTop_nhds_zero_nat (𝕜 := ℝ) - · simp - · left - simpa using hx + have h := (Real.continuous_sqrt.tendsto _).comp + ((tendsto_const_nhds (x := ‖x‖ ^ 2)).add (tendsto_one_div_add_atTop_nhds_zero_nat (𝕜 := ℝ))) + simpa only [normPowerSeries_eq, Function.comp_def, add_zero, + Real.sqrt_sq (norm_pos_iff.mpr hx).le] using h lemma normPowerSeries_inv_tendsto {d} (x : Space d) (hx : x ≠ 0) : - Filter.Tendsto (fun n => (normPowerSeries n x)⁻¹) Filter.atTop (𝓝 (‖x‖⁻¹)) := by - apply Filter.Tendsto.inv₀ - · exact normPowerSeries_tendsto x hx - · simpa using hx + Filter.Tendsto (fun n => (normPowerSeries n x)⁻¹) Filter.atTop (𝓝 (‖x‖⁻¹)) := + (normPowerSeries_tendsto x hx).inv₀ (norm_ne_zero_iff.mpr hx) /-! @@ -159,26 +140,19 @@ open Space lemma deriv_normPowerSeries {d} (n : ℕ) (x : Space d) (i : Fin d) : ∂[i] (normPowerSeries n) x = x i * (normPowerSeries n x)⁻¹ := by - rw [deriv_eq_fderiv_basis, normPowerSeries_eq] - rw [fderiv_sqrt] + rw [deriv_eq_fderiv_basis, normPowerSeries_eq, fderiv_sqrt] simp only [one_div, mul_inv_rev, fderiv_add_const, FunLike.coe_smul, Pi.smul_apply, smul_eq_mul] - rw [← deriv_eq_fderiv_basis] - rw [deriv_norm_sq] + rw [← deriv_eq_fderiv_basis, deriv_norm_sq] ring - · simp - apply DifferentiableAt.norm_sq ℝ - fun_prop + · exact ((differentiable_id.norm_sq ℝ).add_const _).differentiableAt · positivity lemma fderiv_normPowerSeries {d} (n : ℕ) (x y : Space d) : fderiv ℝ (fun (x : Space d) => normPowerSeries n x) x y = ⟪y, x⟫_ℝ * (normPowerSeries n x)⁻¹ := by rw [fderiv_eq_sum_deriv, inner_eq_sum, Finset.sum_mul] - congr - funext i - simp [deriv_normPowerSeries] - ring + exact Finset.sum_congr rfl fun i _ => by simp [deriv_normPowerSeries, mul_assoc] /-! @@ -188,18 +162,14 @@ lemma fderiv_normPowerSeries {d} (n : ℕ) (x y : Space d) : lemma deriv_normPowerSeries_tendsto {d} (x : Space d) (hx : x ≠ 0) (i : Fin d) : Filter.Tendsto (fun n => ∂[i] (normPowerSeries n) x) Filter.atTop (𝓝 (x i * (‖x‖)⁻¹)) := by - conv => enter [1, n]; rw [deriv_normPowerSeries] - refine Filter.Tendsto.mul ?_ ?_ - · exact tendsto_const_nhds - · exact normPowerSeries_inv_tendsto x hx + simp only [deriv_normPowerSeries] + exact tendsto_const_nhds.mul (normPowerSeries_inv_tendsto x hx) lemma fderiv_normPowerSeries_tendsto {d} (x y : Space d) (hx : x ≠ 0) : Filter.Tendsto (fun n => fderiv ℝ (fun (x : Space d) => normPowerSeries n x) x y) Filter.atTop (𝓝 (⟪y, x⟫_ℝ * (‖x‖)⁻¹)) := by - conv => enter [1, n]; rw [fderiv_normPowerSeries] - refine Filter.Tendsto.mul ?_ ?_ - · exact tendsto_const_nhds - · exact normPowerSeries_inv_tendsto x hx + simp only [fderiv_normPowerSeries] + exact tendsto_const_nhds.mul (normPowerSeries_inv_tendsto x hx) /-! @@ -209,11 +179,8 @@ lemma fderiv_normPowerSeries_tendsto {d} (x y : Space d) (hx : x ≠ 0) : @[fun_prop] lemma normPowerSeries_aestronglyMeasurable {d} (n : ℕ) : - AEStronglyMeasurable (normPowerSeries n : Space d → ℝ) volume := by - rw [normPowerSeries_eq_rpow] - refine StronglyMeasurable.aestronglyMeasurable ?_ - refine stronglyMeasurable_iff_measurable.mpr ?_ - fun_prop + AEStronglyMeasurable (normPowerSeries n : Space d → ℝ) volume := + (normPowerSeries_differentiable n).continuous.aestronglyMeasurable /-! @@ -223,98 +190,61 @@ lemma normPowerSeries_aestronglyMeasurable {d} (n : ℕ) : @[simp] lemma normPowerSeries_nonneg {d} (n : ℕ) (x : Space d) : - 0 ≤ normPowerSeries n x := by - rw [normPowerSeries_eq] - simp + 0 ≤ normPowerSeries n x := + Real.sqrt_nonneg _ @[simp] lemma normPowerSeries_pos {d} (n : ℕ) (x : Space d) : - 0 < normPowerSeries n x := by - rw [normPowerSeries_eq] - simp only [one_div, Real.sqrt_pos] - positivity + 0 < normPowerSeries n x := + Real.sqrt_pos_of_pos (by positivity) @[simp] lemma normPowerSeries_ne_zero {d} (n : ℕ) (x : Space d) : - normPowerSeries n x ≠ 0 := by - rw [normPowerSeries_eq] - simp only [one_div, ne_eq] - positivity + normPowerSeries n x ≠ 0 := + (normPowerSeries_pos n x).ne' lemma normPowerSeries_le_norm_sq_add_one {d} (n : ℕ) (x : Space d) : normPowerSeries n x ≤ ‖x‖ + 1 := by - trans √(‖x‖ ^ 2 + 1) - · rw [normPowerSeries_eq] - apply Real.sqrt_le_sqrt - simp only [one_div, add_le_add_iff_left] - refine inv_le_one_iff₀.mpr ?_ - right - simp - · refine (Real.sqrt_le_left (by positivity)).mpr ?_ - trans (‖x‖ ^ 2 + 1) + (2 * ‖x‖) - · simp - · ring_nf - rfl + rw [normPowerSeries_eq] + refine (Real.sqrt_le_left (by positivity)).mpr ?_ + have h : 1 / ((n : ℝ) + 1) ≤ 1 := div_le_one_of_le₀ (by simp) (by positivity) + nlinarith [norm_nonneg x] @[simp] lemma norm_lt_normPowerSeries {d} (n : ℕ) (x : Space d) : - ‖x‖ < normPowerSeries n x := by - rw [normPowerSeries_eq] - apply Real.lt_sqrt_of_sq_lt - simp only [one_div, lt_add_iff_pos_right, inv_pos] - positivity + ‖x‖ < normPowerSeries n x := + Real.lt_sqrt_of_sq_lt (lt_add_of_pos_right _ (by positivity)) lemma norm_le_normPowerSeries {d} (n : ℕ) (x : Space d) : - ‖x‖ ≤ normPowerSeries n x := by - rw [normPowerSeries_eq] - apply Real.le_sqrt_of_sq_le - simp only [one_div, le_add_iff_nonneg_right, inv_nonneg] - positivity + ‖x‖ ≤ normPowerSeries n x := + (norm_lt_normPowerSeries n x).le lemma normPowerSeries_zpow_le_norm_sq_add_one {d} (n : ℕ) (m : ℤ) (x : Space d) (hx : x ≠ 0) : (normPowerSeries n x) ^ m ≤ (‖x‖ + 1) ^ m + ‖x‖ ^ m := by match m with | .ofNat m => - trans (‖x‖ + 1) ^ m - · simp - exact pow_le_pow_left₀ (by simp) (normPowerSeries_le_norm_sq_add_one n x) m - · simp + simpa using le_add_of_le_of_nonneg + (pow_le_pow_left₀ (by simp) (normPowerSeries_le_norm_sq_add_one n x) m) (by positivity) | .negSucc m => - trans (‖x‖ ^ (m + 1))⁻¹; swap - · simp - positivity simp only [zpow_negSucc] - refine inv_anti₀ ?_ ?_ - · positivity - exact pow_le_pow_left₀ (by simp) (norm_le_normPowerSeries n x) (m + 1) + exact le_add_of_nonneg_of_le (by positivity) (inv_anti₀ (by positivity) + (pow_le_pow_left₀ (by simp) (norm_le_normPowerSeries n x) (m + 1))) lemma normPowerSeries_inv_le {d} (n : ℕ) (x : Space d) (hx : x ≠ 0) : - (normPowerSeries n x)⁻¹ ≤ ‖x‖⁻¹ := by - refine inv_anti₀ ?_ ?_ - · positivity - apply Real.le_sqrt_of_sq_le - simp only [one_div, le_add_iff_nonneg_right, inv_nonneg] - positivity + (normPowerSeries n x)⁻¹ ≤ ‖x‖⁻¹ := + inv_anti₀ (norm_pos_iff.mpr hx) (norm_le_normPowerSeries n x) lemma normPowerSeries_log_le_normPowerSeries {d} (n : ℕ) (x : Space d) : |Real.log (normPowerSeries n x)| ≤ (normPowerSeries n x)⁻¹ + (normPowerSeries n x) := by - have h1 := Real.neg_inv_le_log (x := (normPowerSeries n x)) (by simp) - have h2 := Real.log_le_rpow_div (x := (normPowerSeries n x)) (by simp) (ε := 1) (by positivity) rw [abs_le'] - generalize Real.log ‖x‖ = r at * - apply And.intro - · apply h2.trans - simp - · rw [neg_le] - apply le_trans _ h1 - simp + exact ⟨(Real.log_le_rpow_div (x := normPowerSeries n x) (by simp) one_pos).trans (by simp), + (neg_le.mp (Real.neg_inv_le_log (normPowerSeries_nonneg n x))).trans + (le_add_of_nonneg_right (normPowerSeries_nonneg n x))⟩ lemma normPowerSeries_log_le {d} (n : ℕ) (x : Space d) (hx : x ≠ 0) : - |Real.log (normPowerSeries n x)| ≤ ‖x‖⁻¹ + (‖x‖ + 1) := by - apply le_trans (normPowerSeries_log_le_normPowerSeries n x) ?_ - apply add_le_add - · exact normPowerSeries_inv_le n x hx - · exact normPowerSeries_le_norm_sq_add_one n x + |Real.log (normPowerSeries n x)| ≤ ‖x‖⁻¹ + (‖x‖ + 1) := + (normPowerSeries_log_le_normPowerSeries n x).trans + (add_le_add (normPowerSeries_inv_le n x hx) (normPowerSeries_le_norm_sq_add_one n x)) /-! @@ -340,64 +270,44 @@ lemma IsDistBounded.normPowerSeries_zpow {d : ℕ} {n : ℕ} (m : ℤ) : simp only [zpow_negSucc] apply IsDistBounded.mono (f := fun (x : Space d) => ((√(1/(n + 1)) : ℝ) ^ (m + 1))⁻¹) · fun_prop - · rw [normPowerSeries_eq_rpow] - refine StronglyMeasurable.aestronglyMeasurable ?_ - refine stronglyMeasurable_iff_measurable.mpr ?_ - fun_prop + · exact (((normPowerSeries_differentiable n).continuous.pow _).inv₀ + fun x => pow_ne_zero _ (normPowerSeries_ne_zero n x)).aestronglyMeasurable · intro x simp only [norm_inv, norm_pow, Real.norm_eq_abs, one_div] - refine inv_anti₀ (by positivity) ?_ - refine (pow_le_pow_iff_left₀ (by positivity) (by positivity) (by simp)).mpr ?_ - rw [abs_of_nonneg (by positivity), abs_of_nonneg (by simp)] - rw [normPowerSeries_eq] - simp only [Real.sqrt_inv, one_div] - rw [← Real.sqrt_inv] - apply Real.sqrt_le_sqrt - simp + refine inv_anti₀ (by positivity) (pow_le_pow_left₀ (abs_nonneg _) ?_ _) + rw [abs_of_nonneg (by positivity), abs_of_nonneg (by simp), normPowerSeries_eq] + exact Real.sqrt_le_sqrt (by simp) @[fun_prop] lemma IsDistBounded.normPowerSeries_single {d : ℕ} {n : ℕ} : IsDistBounded (d := d) (fun x => (normPowerSeries n x)) := by - convert IsDistBounded.normPowerSeries_zpow (n := n) (m := 1) using 1 - simp + simpa using IsDistBounded.normPowerSeries_zpow (n := n) (m := 1) @[fun_prop] lemma IsDistBounded.normPowerSeries_inv {d : ℕ} {n : ℕ} : IsDistBounded (d := d) (fun x => (normPowerSeries n x)⁻¹) := by - convert normPowerSeries_zpow (n := n) (-1) using 1 - simp + simpa using normPowerSeries_zpow (n := n) (-1) @[fun_prop] lemma IsDistBounded.normPowerSeries_deriv {d : ℕ} (n : ℕ) (i : Fin d) : IsDistBounded (d := d) (fun x => ∂[i] (normPowerSeries n) x) := by - conv => - enter [1, x]; - rw [deriv_normPowerSeries] + simp only [deriv_normPowerSeries] fun_prop @[fun_prop] lemma IsDistBounded.normPowerSeries_fderiv {d : ℕ} (n : ℕ) (y : Space d) : IsDistBounded (d := d) (fun x => fderiv ℝ (fun (x : Space d) => normPowerSeries n x) x y) := by - conv => - enter [1, x]; - rw [fderiv_eq_sum_deriv] - apply IsDistBounded.sum_fun - fun_prop + simp only [fderiv_eq_sum_deriv] + exact IsDistBounded.sum_fun (by fun_prop) @[fun_prop] lemma IsDistBounded.normPowerSeries_log {d : ℕ} (n : ℕ) : IsDistBounded (d := d) (fun x => Real.log (normPowerSeries n x)) := by apply IsDistBounded.mono (f := fun x => (normPowerSeries n x)⁻¹ + (normPowerSeries n x)) · fun_prop - · apply AEMeasurable.aestronglyMeasurable - fun_prop - · intro x - simp only [Real.norm_eq_abs] - conv_rhs => rw [abs_of_nonneg (by - apply add_nonneg - · simp - · simp)] - exact normPowerSeries_log_le_normPowerSeries n x + · exact ((normPowerSeries_differentiable n).continuous.log + (normPowerSeries_ne_zero n)).aestronglyMeasurable + · exact fun x => (normPowerSeries_log_le_normPowerSeries n x).trans (le_abs_self _) /-! @@ -407,26 +317,18 @@ lemma IsDistBounded.normPowerSeries_log {d : ℕ} (n : ℕ) : @[fun_prop] lemma differentiable_normPowerSeries_zpow {d : ℕ} {n : ℕ} (m : ℤ) : - Differentiable ℝ (fun x : Space d => (normPowerSeries n x) ^ m) := by - refine Differentiable.zpow ?_ ?_ - · fun_prop - · left - exact normPowerSeries_ne_zero n + Differentiable ℝ (fun x : Space d => (normPowerSeries n x) ^ m) := + Differentiable.zpow (by fun_prop) (.inl (normPowerSeries_ne_zero n)) @[fun_prop] lemma differentiable_normPowerSeries_inv {d : ℕ} {n : ℕ} : - Differentiable ℝ (fun x : Space d => (normPowerSeries n x)⁻¹) := by - convert differentiable_normPowerSeries_zpow (n := n) (m := -1) using 1 - funext x - simp + Differentiable ℝ (fun x : Space d => (normPowerSeries n x)⁻¹) := + Differentiable.inv (by fun_prop) (normPowerSeries_ne_zero n) @[fun_prop] lemma differentiable_log_normPowerSeries {d : ℕ} {n : ℕ} : - Differentiable ℝ (fun x : Space d => Real.log (normPowerSeries n x)) := by - refine Differentiable.log ?_ ?_ - · fun_prop - · intro x - exact normPowerSeries_ne_zero n x + Differentiable ℝ (fun x : Space d => Real.log (normPowerSeries n x)) := + Differentiable.log (by fun_prop) (normPowerSeries_ne_zero n) /-! ### A.9. Derivatives of functions @@ -438,57 +340,39 @@ lemma deriv_normPowerSeries_zpow {d : ℕ} {n : ℕ} (m : ℤ) (x : Space d) (i m * x i * (normPowerSeries n x) ^ (m - 2) := by rw [deriv_eq_fderiv_basis] change (fderiv ℝ ((fun x => x ^ m) ∘ normPowerSeries n) x) (basis i) = _ - rw [fderiv_comp] + rw [show m - 2 = m - 1 - 1 by ring, zpow_sub_one₀ (normPowerSeries_ne_zero n x), fderiv_comp] simp only [ContinuousLinearMap.coe_comp, Function.comp_apply, fderiv_eq_smul_deriv, deriv_zpow', smul_eq_mul] - rw [fderiv_normPowerSeries] - simp only [basis_inner] - field_simp - ring_nf - have h1 : normPowerSeries n x ^ (-1 + m) = normPowerSeries n x ^ ((-2 + m) + 1) := by ring_nf - rw [h1, zpow_add₀] - simp only [Int.reduceNeg, zpow_one] + rw [fderiv_normPowerSeries, basis_inner] ring - · simp - · refine DifferentiableAt.zpow ?_ ?_ - · fun_prop - · left - exact normPowerSeries_ne_zero n x + · exact differentiableAt_zpow.mpr (.inl (normPowerSeries_ne_zero n x)) · fun_prop lemma fderiv_normPowerSeries_zpow {d : ℕ} {n : ℕ} (m : ℤ) (x y : Space d) : fderiv ℝ (fun x : Space d => (normPowerSeries n x) ^ m) x y = m * ⟪y, x⟫_ℝ * (normPowerSeries n x) ^ (m - 2) := by rw [fderiv_eq_sum_deriv, inner_eq_sum, Finset.mul_sum, Finset.sum_mul] - congr - funext i - simp [deriv_normPowerSeries_zpow] - ring + exact Finset.sum_congr rfl fun i _ => by + simp [deriv_normPowerSeries_zpow, mul_assoc, mul_comm, mul_left_comm] lemma deriv_log_normPowerSeries {d : ℕ} {n : ℕ} (x : Space d) (i : Fin d) : ∂[i] (fun x : Space d => Real.log (normPowerSeries n x)) x = x i * (normPowerSeries n x) ^ (-2 : ℤ) := by rw [deriv_eq_fderiv_basis] change (fderiv ℝ (Real.log ∘ normPowerSeries n) x) (basis i) = _ - rw [fderiv_comp,] + rw [fderiv_comp] simp only [ContinuousLinearMap.coe_comp, Function.comp_apply, fderiv_eq_smul_deriv, Real.deriv_log', smul_eq_mul, Int.reduceNeg, zpow_neg] - rw [fderiv_normPowerSeries] - simp [zpow_ofNat, sq] + simp [fderiv_normPowerSeries, zpow_ofNat, sq] ring - · apply DifferentiableAt.log ?_ ?_ - · fun_prop - exact normPowerSeries_ne_zero n x + · exact Real.differentiableAt_log (normPowerSeries_ne_zero n x) · fun_prop lemma fderiv_log_normPowerSeries {d : ℕ} {n : ℕ} (x y : Space d) : fderiv ℝ (fun x : Space d => Real.log (normPowerSeries n x)) x y = ⟪y, x⟫_ℝ * (normPowerSeries n x) ^ (-2 : ℤ) := by rw [fderiv_eq_sum_deriv, inner_eq_sum, Finset.sum_mul] - congr - funext i - simp [deriv_log_normPowerSeries] - ring + exact Finset.sum_congr rfl fun i _ => by simp [deriv_log_normPowerSeries, mul_assoc] /-! @@ -501,8 +385,7 @@ lemma gradient_dist_normPowerSeries_zpow {d : ℕ} {n : ℕ} (m : ℤ) : distOfFunction (fun x : Space d => (m * (normPowerSeries n x) ^ (m - 2)) • basis.repr x) (by fun_prop) := by ext1 η - apply ext_inner_right ℝ - intro y + refine ext_inner_right ℝ fun y => ?_ simp [distGrad_inner_eq] rw [Distribution.fderivD_apply, distOfFunction_apply, distOfFunction_inner] calc _ @@ -511,19 +394,14 @@ lemma gradient_dist_normPowerSeries_zpow {d : ℕ} {n : ℕ} (m : ℤ) : rw [integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable] · fun_prop · refine IsDistBounded.integrable_space_mul ?_ η - conv => enter [1, x]; rw [fderiv_normPowerSeries_zpow] - simp [mul_assoc] + simp only [fderiv_normPowerSeries_zpow, mul_assoc] fun_prop · fun_prop · fun_prop - · intro _ _ - apply Differentiable.differentiableAt - fun_prop + · exact fun _ _ => (differentiable_normPowerSeries_zpow m).differentiableAt _ = ∫ (x : Space d), η x * (m * ⟪(basis.repr.symm y), x⟫_ℝ * (normPowerSeries n x) ^ (m - 2)) := by - congr - funext x - rw [fderiv_normPowerSeries_zpow] + simp only [fderiv_normPowerSeries_zpow] congr funext x simp [inner_smul_left_eq_smul] @@ -554,48 +432,23 @@ lemma gradient_dist_normPowerSeries_zpow_tendsTo_distGrad_norm {d : ℕ} [NeZero apply MeasureTheory.tendsto_integral_of_dominated_convergence (bound := fun x => |fderiv ℝ η x (basis.repr.symm y)| * ((‖x‖ + 1) ^ m + ‖x‖ ^ m)) · intro n - apply IsDistBounded.aeStronglyMeasurable_fderiv_schwartzMap_smul (F := ℝ) ?_ - fun_prop + exact IsDistBounded.aeStronglyMeasurable_fderiv_schwartzMap_smul (F := ℝ) (by fun_prop) η _ · have h1 : Integrable (fun x => (fderiv ℝ (⇑η) x) (basis.repr.symm y) * ((‖x‖ + 1) ^ m + ‖x‖ ^ m)) volume := by - apply IsDistBounded.integrable_space_fderiv ?_ - apply IsDistBounded.add - · refine IsDistBounded.norm_add_pos_nat_zpow m 1 ?_ - simp - · exact IsDistBounded.pow m hm - rw [← integrable_norm_iff] at h1 - convert h1 using 1 - funext x - simp only [norm_mul, Real.norm_eq_abs, mul_eq_mul_left_iff, abs_eq_zero] - left - rw [abs_of_nonneg (by positivity)] - fun_prop + apply IsDistBounded.integrable_space_fderiv + ((IsDistBounded.norm_add_pos_nat_zpow m 1 one_pos).add (IsDistBounded.pow m hm)) + refine h1.abs.congr (ae_of_all _ fun x => ?_) + simp only [abs_mul] + congr 1 + exact abs_of_nonneg (by positivity) · intro n - rw [Filter.eventually_iff_exists_mem] - use {0}ᶜ - constructor - · rw [compl_mem_ae_iff, measure_singleton] - intro x hx - simp at hx - simp - apply mul_le_mul (by rfl) _ (by positivity) (by positivity) - rw [abs_of_nonneg (by simp)] - exact normPowerSeries_zpow_le_norm_sq_add_one n m x hx - · rw [Filter.eventually_iff_exists_mem] - use {0}ᶜ - constructor - · rw [compl_mem_ae_iff, measure_singleton] - intro x hx - apply Filter.Tendsto.mul - · exact tendsto_const_nhds - have h1 : Filter.Tendsto (fun x_1 => normPowerSeries x_1 x ^ (m : ℝ)) - Filter.atTop (𝓝 (‖x‖ ^ (m : ℝ))) := by - refine Filter.Tendsto.rpow ?_ ?_ ?_ - · apply normPowerSeries_tendsto x hx - · simp - · left - simpa using hx - simpa using h1 + filter_upwards [Measure.ae_ne volume 0] with x hx + simp [abs_of_nonneg (normPowerSeries_nonneg n x)] + exact mul_le_mul_of_nonneg_left + (normPowerSeries_zpow_le_norm_sq_add_one n m x hx) (abs_nonneg _) + · filter_upwards [Measure.ae_ne volume 0] with x hx + exact tendsto_const_nhds.mul + ((normPowerSeries_tendsto x hx).zpow₀ m (.inl (norm_ne_zero_iff.mpr hx))) lemma gradient_dist_normPowerSeries_zpow_tendsTo {d : ℕ} [NeZero d] (m : ℤ) (hm : - (d - 1 : ℕ) + 1 ≤ m) @@ -609,28 +462,21 @@ lemma gradient_dist_normPowerSeries_zpow_tendsTo {d : ℕ} [NeZero d] (m : ℤ) refine IsDistBounded.const_fun_smul ?_ ↑m apply IsDistBounded.zpow_smul_repr_self omega) η, y⟫_ℝ)) := by - conv => - enter [1, n]; - rw [gradient_dist_normPowerSeries_zpow] + simp only [gradient_dist_normPowerSeries_zpow] simp [distOfFunction_inner] have h1 (n : ℕ) (x : Space d) : η x * ⟪(↑m * normPowerSeries n x ^ (m - 2)) • basis.repr x, (y)⟫_ℝ = η x * (m * (⟪basis.repr x, y⟫_ℝ * (normPowerSeries n x) ^ (m - 2))) := by - simp [inner_smul_left] - ring_nf - left - trivial - conv => - enter [1, n, 2, x]; - rw [h1 n x] + rw [real_inner_smul_left] + ring + simp only [h1] apply MeasureTheory.tendsto_integral_of_dominated_convergence (bound := fun x => |η x| * |m| * |⟪basis.repr x, y⟫_ℝ| * ((‖x‖ + 1) ^ (m - 2) + ‖x‖ ^ (m - 2))) · intro n apply IsDistBounded.aeStronglyMeasurable_schwartzMap_smul (F := ℝ) ?_ η apply IsDistBounded.const_mul_fun simp [basis_repr_inner_eq] - apply IsDistBounded.isDistBounded_mul_inner' - fun_prop + exact IsDistBounded.isDistBounded_mul_inner' (by fun_prop) _ · have h1 : Integrable (fun x => η x * (m * (⟪basis.repr x, y⟫_ℝ * ((‖x‖ + 1) ^ (m - 2) + ‖x‖ ^ (m - 2))))) volume := by apply IsDistBounded.integrable_space_mul ?_ η @@ -638,21 +484,16 @@ lemma gradient_dist_normPowerSeries_zpow_tendsTo {d : ℕ} [NeZero d] (m : ℤ) simp [mul_add] apply IsDistBounded.add · simp [basis_repr_inner_eq] - apply IsDistBounded.isDistBounded_mul_inner' - refine IsDistBounded.norm_add_pos_nat_zpow (m - 2) 1 ?_ - simp + exact IsDistBounded.isDistBounded_mul_inner' + (IsDistBounded.norm_add_pos_nat_zpow (m - 2) 1 one_pos) _ · simp [basis_repr_inner_eq] conv => enter [1, x] rw [real_inner_comm] apply IsDistBounded.isDistBounded_mul_inner_of_smul_norm · apply IsDistBounded.mono (f := fun x => ‖x‖ ^ (m - 1) + 1) - · apply IsDistBounded.add - · apply IsDistBounded.pow (m - 1) - omega - · fun_prop - · apply AEMeasurable.aestronglyMeasurable - fun_prop + · exact (IsDistBounded.pow (m - 1) (by omega)).add (by fun_prop) + · exact AEMeasurable.aestronglyMeasurable (by fun_prop) · intro x simp only [norm_mul, Real.norm_eq_abs, abs_norm, norm_zpow] rw [abs_of_nonneg (by positivity)] @@ -660,60 +501,27 @@ lemma gradient_dist_normPowerSeries_zpow_tendsTo {d : ℕ} [NeZero d] (m : ℤ) · subst hx simp [zero_zpow_eq] split_ifs <;> grind - · trans ‖x‖ ^ (m - 1); swap - · simp - apply le_of_eq - trans ‖x‖ ^ (m - 2 + 1) - rw [zpow_add₀, zpow_one] - ring - simpa using hx - ring_nf - · apply AEMeasurable.aestronglyMeasurable - fun_prop - rw [← integrable_norm_iff] at h1 - convert h1 using 1 - funext x - simp [mul_assoc] - rw [abs_of_nonneg (by positivity)] - simp only [true_or] - fun_prop + · rw [mul_comm, ← zpow_add_one₀ (norm_ne_zero_iff.mpr hx), + show m - 2 + 1 = m - 1 by ring] + simp + · exact AEMeasurable.aestronglyMeasurable (by fun_prop) + refine h1.abs.congr (ae_of_all _ fun x => ?_) + simp only [abs_mul, mul_assoc, Int.cast_abs, + abs_of_nonneg (show (0:ℝ) ≤ (‖x‖ + 1) ^ (m - 2) + ‖x‖ ^ (m - 2) by positivity)] · intro n - rw [Filter.eventually_iff_exists_mem] - use {0}ᶜ - constructor - · rw [compl_mem_ae_iff, measure_singleton] - intro x hx - simp at hx + filter_upwards [Measure.ae_ne volume 0] with x hx simp [mul_assoc] - apply mul_le_mul (by rfl) _ (by positivity) (by positivity) - apply mul_le_mul (by rfl) _ (by positivity) (by positivity) - apply mul_le_mul (by rfl) _ (by positivity) (by positivity) + gcongr rw [abs_of_nonneg (by simp)] exact normPowerSeries_zpow_le_norm_sq_add_one n (m - 2) x hx - · rw [Filter.eventually_iff_exists_mem] - use {0}ᶜ - constructor - · rw [compl_mem_ae_iff, measure_singleton] - intro x hx - apply Filter.Tendsto.mul - · exact tendsto_const_nhds - simp [inner_smul_left, mul_assoc] - apply Filter.Tendsto.mul - · exact tendsto_const_nhds - ring_nf - apply Filter.Tendsto.mul - · exact tendsto_const_nhds - have h1 : Filter.Tendsto (fun x_1 => normPowerSeries x_1 x ^ ((m - 2 : ℤ) : ℝ)) - Filter.atTop (𝓝 (‖x‖ ^ ((m - 2 : ℤ) : ℝ))) := by - refine Filter.Tendsto.rpow ?_ ?_ ?_ - · apply normPowerSeries_tendsto x hx - · simp - · left - simpa using hx - simp [-Int.cast_sub, Real.rpow_intCast] at h1 - convert h1 using 3 - · ring - · ring + · filter_upwards [Measure.ae_ne volume 0] with x hx + have h2 : ⟪((m : ℝ) * ‖x‖ ^ (m - 2)) • basis.repr x, y⟫_ℝ = + (m : ℝ) * (⟪basis.repr x, y⟫_ℝ * ‖x‖ ^ (m - 2)) := by + rw [real_inner_smul_left] + ring + rw [h2] + exact tendsto_const_nhds.mul (tendsto_const_nhds.mul (tendsto_const_nhds.mul + ((normPowerSeries_tendsto x hx).zpow₀ _ (.inl (norm_ne_zero_iff.mpr hx))))) /-! @@ -726,8 +534,7 @@ lemma gradient_dist_normPowerSeries_log {d : ℕ} {n : ℕ} : distOfFunction (fun x : Space d => ((normPowerSeries n x) ^ (- 2 : ℤ)) • basis.repr x) (by fun_prop) := by ext1 η - apply ext_inner_right ℝ - intro y + refine ext_inner_right ℝ fun y => ?_ simp [distGrad_inner_eq] rw [Distribution.fderivD_apply, distOfFunction_apply, distOfFunction_inner] calc _ @@ -737,23 +544,18 @@ lemma gradient_dist_normPowerSeries_log {d : ℕ} {n : ℕ} : rw [integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable] · fun_prop · refine IsDistBounded.integrable_space_mul ?_ η - conv => enter [1, x]; rw [fderiv_log_normPowerSeries] + simp only [fderiv_log_normPowerSeries] fun_prop · fun_prop · fun_prop - · intro _ _ - apply Differentiable.differentiableAt - fun_prop + · exact fun _ _ => Differentiable.differentiableAt (by fun_prop) _ = ∫ (x : Space d), η x * (⟪basis.repr.symm y, x⟫_ℝ * (normPowerSeries n x) ^ (- 2 : ℤ)) := by - congr - funext x - rw [fderiv_log_normPowerSeries] + simp only [fderiv_log_normPowerSeries] congr funext x simp [inner_smul_left_eq_smul] left - rw [real_inner_comm] - rw [basis_repr_inner_eq] + rw [real_inner_comm, basis_repr_inner_eq] ring /-! @@ -779,40 +581,22 @@ lemma gradient_dist_normPowerSeries_log_tendsTo_distGrad_norm {d : ℕ} (hd : 2 apply MeasureTheory.tendsto_integral_of_dominated_convergence (bound := fun x => |fderiv ℝ η x (basis.repr.symm y)| * (‖x‖⁻¹ + (‖x‖ + 1))) · intro n - apply IsDistBounded.aeStronglyMeasurable_fderiv_schwartzMap_smul (F := ℝ) ?_ - fun_prop + exact IsDistBounded.aeStronglyMeasurable_fderiv_schwartzMap_smul (F := ℝ) (by fun_prop) η _ · have h1 : Integrable (fun x => (fderiv ℝ (⇑η) x) (basis.repr.symm y) * (‖x‖⁻¹ + (‖x‖ + 1))) volume := by - apply IsDistBounded.integrable_space_fderiv ?_ - apply IsDistBounded.add - · exact IsDistBounded.inv - · fun_prop - rw [← integrable_norm_iff] at h1 - convert h1 using 1 - funext x - simp only [norm_mul, Real.norm_eq_abs, mul_eq_mul_left_iff, abs_eq_zero] - left - rw [abs_of_nonneg (by positivity)] - fun_prop + apply IsDistBounded.integrable_space_fderiv + (IsDistBounded.add IsDistBounded.inv (by fun_prop)) + refine h1.abs.congr (ae_of_all _ fun x => ?_) + simp only [abs_mul] + congr 1 + exact abs_of_nonneg (by positivity) · intro n - rw [Filter.eventually_iff_exists_mem] - use {0}ᶜ - constructor - · rw [compl_mem_ae_iff, measure_singleton] - intro x hx - simp at hx + filter_upwards [Measure.ae_ne volume 0] with x hx simp - exact mul_le_mul (by rfl) (normPowerSeries_log_le n x hx) (by positivity) (by positivity) - · rw [Filter.eventually_iff_exists_mem] - use {0}ᶜ - constructor - · rw [compl_mem_ae_iff, measure_singleton] - intro x hx - apply Filter.Tendsto.mul - · exact tendsto_const_nhds - apply Filter.Tendsto.log - · exact normPowerSeries_tendsto x hx - · simpa using hx + exact mul_le_mul_of_nonneg_left (normPowerSeries_log_le n x hx) (abs_nonneg _) + · filter_upwards [Measure.ae_ne volume 0] with x hx + exact tendsto_const_nhds.mul + ((normPowerSeries_tendsto x hx).log (norm_ne_zero_iff.mpr hx)) lemma gradient_dist_normPowerSeries_log_tendsTo {d : ℕ} (hd : 2 ≤ d) (η : 𝓢(Space d, ℝ)) (y : EuclideanSpace ℝ (Fin d)) : @@ -824,78 +608,48 @@ lemma gradient_dist_normPowerSeries_log_tendsTo {d : ℕ} (hd : 2 ≤ d) refine (IsDistBounded.zpow_smul_repr_self _ ?_) omega) η, y⟫_ℝ)) := by haveI : NeZero d := ⟨by omega⟩ - conv => - enter [1, n]; - rw [gradient_dist_normPowerSeries_log] - simp only [distOfFunction_inner] + simp only [gradient_dist_normPowerSeries_log, distOfFunction_inner] have h1 (n : ℕ) (x : Space d) : η x * ⟪(normPowerSeries n x ^ (- 2 : ℤ)) • basis.repr x, y⟫_ℝ = η x * ((⟪basis.repr x, y⟫_ℝ * (normPowerSeries n x) ^ (- 2 : ℤ))) := by - simp [inner_smul_left] - ring_nf - left - trivial - conv => - enter [1, n, 2, x] - rw [h1 n x] + rw [real_inner_smul_left] + ring + simp only [h1] apply MeasureTheory.tendsto_integral_of_dominated_convergence (bound := fun x => |η x| * |⟪basis.repr x, y⟫_ℝ| * ((‖x‖ + 1) ^ (- 2 : ℤ) + ‖x‖ ^ (- 2 : ℤ))) · intro n - apply IsDistBounded.aeStronglyMeasurable_schwartzMap_smul (F := ℝ) ?_ η + refine IsDistBounded.aeStronglyMeasurable_schwartzMap_smul (F := ℝ) ?_ η simp only [basis_repr_inner_eq] - apply IsDistBounded.isDistBounded_mul_inner' - fun_prop + exact IsDistBounded.isDistBounded_mul_inner' (by fun_prop) _ · have h1 : Integrable (fun x => η x * ((⟪basis.repr x, y⟫_ℝ * ((‖x‖ + 1) ^ (- 2 : ℤ) + ‖x‖ ^ (- 2 : ℤ))))) volume := by apply IsDistBounded.integrable_space_mul ?_ η simp [mul_add] apply IsDistBounded.add · simp only [basis_repr_inner_eq] - apply IsDistBounded.isDistBounded_mul_inner' - refine IsDistBounded.norm_add_pos_nat_zpow (- 2) 1 ?_ - simp + exact IsDistBounded.isDistBounded_mul_inner' + (IsDistBounded.norm_add_pos_nat_zpow (- 2) 1 one_pos) _ · simp only [basis_repr_inner_eq] convert IsDistBounded.mul_inner_pow_neg_two (basis.repr.symm y) using 1 funext x simp [real_inner_comm] - rw [← integrable_norm_iff] at h1 - convert h1 using 1 - funext x - simp [mul_assoc] - rw [abs_of_nonneg (by positivity)] - simp only [true_or] - fun_prop + refine h1.abs.congr (ae_of_all _ fun x => ?_) + simp only [abs_mul, mul_assoc, + abs_of_nonneg (show (0:ℝ) ≤ (‖x‖ + 1) ^ (- 2 : ℤ) + ‖x‖ ^ (- 2 : ℤ) by positivity)] · intro n - rw [Filter.eventually_iff_exists_mem] - use {0}ᶜ - constructor - · rw [compl_mem_ae_iff, measure_singleton] - intro x hx - simp at hx + filter_upwards [Measure.ae_ne volume 0] with x hx simp [mul_assoc] - apply mul_le_mul (by rfl) _ (by positivity) (by positivity) - apply mul_le_mul (by rfl) _ (by positivity) (by positivity) + gcongr rw [abs_of_nonneg (by simp)] exact normPowerSeries_zpow_le_norm_sq_add_one n (- 2 : ℤ) x hx - · rw [Filter.eventually_iff_exists_mem] - use {0}ᶜ - constructor - · rw [compl_mem_ae_iff, measure_singleton] - intro x hx - apply Filter.Tendsto.mul - · exact tendsto_const_nhds - simp [inner_smul_left, inner_smul_left] - rw [mul_comm] - apply Filter.Tendsto.mul - · exact tendsto_const_nhds - have h1 : Filter.Tendsto (fun x_1 => normPowerSeries x_1 x ^ ((- 2 : ℤ) : ℝ)) - Filter.atTop (𝓝 (‖x‖ ^ ((- 2 : ℤ) : ℝ))) := by - refine Filter.Tendsto.rpow ?_ ?_ ?_ - · apply normPowerSeries_tendsto x hx - · simp - · left - simpa using hx - simpa using h1 + · filter_upwards [Measure.ae_ne volume 0] with x hx + have h2 : ⟪(‖x‖ ^ (- 2 : ℤ)) • basis.repr x, y⟫_ℝ = + ⟪basis.repr x, y⟫_ℝ * ‖x‖ ^ (- 2 : ℤ) := by + rw [real_inner_smul_left] + ring + rw [h2] + exact tendsto_const_nhds.mul (tendsto_const_nhds.mul + ((normPowerSeries_tendsto x hx).zpow₀ _ (.inl (norm_ne_zero_iff.mpr hx)))) /-! @@ -950,9 +704,8 @@ open Distribution private lemma integrable_real_pow_mul_schwartz (ψ : 𝓢(ℝ, ℝ)) (k : ℕ) : Integrable (fun x : ℝ => x ^ k * ψ x) volume := by - refine (ψ.integrable_pow_mul volume k).mono' (by fun_prop) ?_ - filter_upwards with x - simp [norm_mul, norm_pow] + refine (ψ.integrable_pow_mul volume k).mono' (by fun_prop) + (ae_of_all _ fun x => by simp [norm_mul, norm_pow]) private lemma radial_power_deriv_integral_by_parts {d : ℕ} (η : 𝓢(Space d, ℝ)) @@ -976,9 +729,7 @@ private lemma radial_power_deriv_integral_by_parts | 1 => use 0, 1 intro x - simp [fderiv_smul_const, iteratedFDeriv_succ_eq_comp_right] - rw [(continuousMultilinearCurryRightEquiv' ℝ 0 ℝ (Space d)).symm.norm_map] - simp [ContinuousLinearMap.norm_smulRight_apply] + simp [fderiv_smul_const] | n' + 1 + 1 => use 0, 0 intro x @@ -994,35 +745,29 @@ private lemma radial_power_deriv_integral_by_parts ∀ k x, ((Physlib.Distribution.powOneMul ℝ)^[k] η') x = x ^ k * η' x := by intro k induction k with - | zero => - intro x - simp + | zero => simp | succ k ih => - intro x - rw [Function.iterate_succ_apply'] - rw [Physlib.Distribution.powOneMul_apply, ih] - rw [pow_succ] - change x * (x ^ k * η' x) = x ^ k * x * η' x - ring + intro x + rw [Function.iterate_succ_apply', Physlib.Distribution.powOneMul_apply, ih, pow_succ] + change x * (x ^ k * η' x) = x ^ k * x * η' x + ring have hleft_subtype : ∫ (r : Set.Ioi (0 : ℝ)), r.1 ^ p * _root_.deriv (fun a => η (a • n.1)) r.1 ∂(.comap Subtype.val volume) = ∫ (x : ℝ) in Set.Ioi (0 : ℝ), - x ^ p * _root_.deriv (fun a => η (a • n.1)) x := by - exact MeasureTheory.integral_subtype_comap (μ := volume) - (s := Set.Ioi (0 : ℝ)) measurableSet_Ioi - (fun x : ℝ => x ^ p * _root_.deriv (fun a => η (a • n.1)) x) + x ^ p * _root_.deriv (fun a => η (a • n.1)) x := + MeasureTheory.integral_subtype_comap measurableSet_Ioi + fun x : ℝ => x ^ p * _root_.deriv (fun a => η (a • n.1)) x have hright_subtype : ∫ (r : Set.Ioi (0 : ℝ)), r.1 ^ (p - 1) * η (r.1 • n.1) ∂(.comap Subtype.val volume) = ∫ (x : ℝ) in Set.Ioi (0 : ℝ), - x ^ (p - 1) * η (x • n.1) := MeasureTheory.integral_subtype_comap (μ := volume) - (s := Set.Ioi (0 : ℝ)) measurableSet_Ioi - (fun x : ℝ => x ^ (p - 1) * η (x • n.1)) + x ^ (p - 1) * η (x • n.1) := + MeasureTheory.integral_subtype_comap measurableSet_Ioi fun x : ℝ => x ^ (p - 1) * η (x • n.1) rw [hleft_subtype, hright_subtype] have hIBP : ∫ (x : ℝ) in Set.Ioi (0 : ℝ), @@ -1038,49 +783,26 @@ private lemma radial_power_deriv_integral_by_parts (v := fun x : ℝ => η (x • n.1)) (v' := fun x : ℝ => _root_.deriv (fun a => η (a • n.1)) x) (a' := (0 : ℝ)) (b' := (0 : ℝ)) ?_ ?_ ?_ ?_ ?_ ?_ - · intro x hx - simpa using (hasDerivAt_pow p x) - · intro x hx - exact DifferentiableAt.hasDerivAt (by fun_prop : - DifferentiableAt ℝ (fun x : ℝ => η (x • n.1)) x) - · have hderiv_int : - Integrable (fun x : ℝ => - x ^ p * ((SchwartzMap.derivCLM ℝ ℝ) η') x) volume := - integrable_real_pow_mul_schwartz ((SchwartzMap.derivCLM ℝ ℝ) η') p - exact hderiv_int.integrableOn.congr_fun (by - intro x hx - have hderiv_eq : - _root_.deriv η' x = _root_.deriv (fun a => η (a • n.1)) x := by - congr 1 - simp [SchwartzMap.derivCLM_apply, hderiv_eq]) - measurableSet_Ioi - · have hbase : - Integrable (fun x : ℝ => x ^ (p - 1) * η' x) volume := - integrable_real_pow_mul_schwartz η' (p - 1) - have hconst : - Integrable (fun x : ℝ => (p : ℝ) * (x ^ (p - 1) * η' x)) volume := - hbase.const_mul (p : ℝ) - exact hconst.integrableOn.congr_fun (by - intro x hx - ring_nf - simp [hη'_apply, mul_assoc]) - measurableSet_Ioi + · exact fun x _ => by simpa using hasDerivAt_pow p x + · exact fun x _ => DifferentiableAt.hasDerivAt (by fun_prop) + · refine (integrable_real_pow_mul_schwartz ((SchwartzMap.derivCLM ℝ ℝ) η') + p).integrableOn.congr_fun (fun x _ => ?_) measurableSet_Ioi + have hderiv_eq : _root_.deriv η' x = _root_.deriv (fun a => η (a • n.1)) x := by congr 1 + simp [SchwartzMap.derivCLM_apply, hderiv_eq] + · refine ((integrable_real_pow_mul_schwartz η' (p - 1)).const_mul + (p : ℝ)).integrableOn.congr_fun (fun x _ => ?_) measurableSet_Ioi + ring_nf + simp [hη'_apply, mul_assoc] · have hcont : ContinuousAt (fun x : ℝ => x ^ p * η (x • n.1)) (0 : ℝ) := by fun_prop - have hlim := tendsto_nhdsWithin_of_tendsto_nhds - (s := Set.Ioi (0 : ℝ)) hcont.tendsto + have hlim := tendsto_nhdsWithin_of_tendsto_nhds (s := Set.Ioi (0 : ℝ)) hcont.tendsto simp only [ne_eq, hp.ne', not_false_eq_true, zero_pow, zero_smul, zero_mul] at hlim exact hlim - · have hzero : - Filter.Tendsto (fun x : ℝ => x ^ p * η' x) Filter.atTop (𝓝 (0 : ℝ)) := by - have hsch : - Filter.Tendsto (fun x : ℝ => ((Physlib.Distribution.powOneMul ℝ)^[p] η') x) - Filter.atTop (𝓝 (0 : ℝ)) := - Filter.Tendsto.mono_left - (((Physlib.Distribution.powOneMul ℝ)^[p] η').toZeroAtInfty.zero_at_infty') - atTop_le_cocompact - exact hsch.congr' (Filter.Eventually.of_forall (fun x => by - rw [hmul_iter_apply p x])) - exact hzero + · have hsch : Filter.Tendsto (fun x : ℝ => ((Physlib.Distribution.powOneMul ℝ)^[p] η') x) + Filter.atTop (𝓝 (0 : ℝ)) := + Filter.Tendsto.mono_left + (((Physlib.Distribution.powOneMul ℝ)^[p] η').toZeroAtInfty.zero_at_infty') + atTop_le_cocompact + exact hsch.congr' (Filter.Eventually.of_forall (hmul_iter_apply p)) calc -∫ (x : ℝ) in Set.Ioi (0 : ℝ), x ^ p * _root_.deriv (fun a => η (a • n.1)) x @@ -1090,10 +812,7 @@ private lemma radial_power_deriv_integral_by_parts ring _ = (p : ℝ) * ∫ (x : ℝ) in Set.Ioi (0 : ℝ), x ^ (p - 1) * η (x • n.1) := by - rw [← integral_const_mul] - congr - funext x - ring + simp only [mul_assoc, integral_const_mul] private lemma distDiv_norm_zpow_smul_repr_self_apply_eq_radial_deriv {d p : ℕ} [NeZero d] (q : ℤ) (hq : 0 < q + (d : ℤ)) @@ -1136,10 +855,8 @@ private lemma distDiv_norm_zpow_smul_repr_self_apply_eq_radial_deriv rw [NNReal.smul_def] rw [Real.coe_toNNReal _ (pow_nonneg (le_of_lt hr) (d - 1))] · simp only [smul_eq_mul] - rw [hnorm] - rw [← grad_smul_inner_space (n : Space d) (⇑η) - (SchwartzMap.differentiable η) (r : ℝ) hr] - rw [real_inner_comm] + rw [hnorm, ← grad_smul_inner_space (n : Space d) (⇑η) + (SchwartzMap.differentiable η) (r : ℝ) hr, real_inner_comm] simp only [inner_smul_right] rw [← radial_jacobian_zpow_mul_self hp_int hr] ring @@ -1154,9 +871,7 @@ lemma distDiv_norm_zpow_smul_repr_self_eq_smul ext η let p : ℕ := Int.toNat (q + (d : ℤ)) have hp_int : (p : ℤ) = q + (d : ℤ) := by simpa [p] using Int.toNat_of_nonneg (le_of_lt hq) - have hp_pos : 0 < p := by - have : (0 : ℤ) < (p : ℤ) := by simpa [hp_int] using hq - exact_mod_cast this + have hp_pos : 0 < p := by omega have hcoef : (((q + d : ℤ) : ℝ)) = (p : ℝ) := by exact_mod_cast hp_int.symm calc @@ -1186,10 +901,7 @@ lemma distDiv_norm_zpow_smul_repr_self_eq_smul _ = (((q + (d : ℤ) : ℤ) : ℝ) • distOfFunction (fun x : Space d => ‖x‖ ^ q) (IsDistBounded.pow q (by omega))) η := by - simp [distOfFunction_apply, mul_comm] - left - rw [← hcoef] - norm_num + simp [distOfFunction_apply, hcoef] /-! @@ -1204,10 +916,7 @@ lemma distLaplacian_distOfFunction_norm_zpow {d : ℕ} [NeZero d] (m : ℤ) (((m : ℝ) * (((m - 2 + d : ℤ) : ℝ))) • distOfFunction (fun x : Space d => ‖x‖ ^ (m - 2)) (IsDistBounded.pow (m - 2) (by omega))) := by - rw [distLaplacian] - change ∇ᵈ ⬝ (∇ᵈ (distOfFunction (fun x : Space d => ‖x‖ ^ m) - (IsDistBounded.pow m (by omega)))) = _ - rw [distGrad_distOfFunction_norm_zpow m (by omega)] + rw [distLaplacian, LinearMap.comp_apply, distGrad_distOfFunction_norm_zpow m (by omega)] have hdist : distOfFunction (fun x : Space d => (m * ‖x‖ ^ (m - 2)) • basis.repr x) (by @@ -1223,10 +932,7 @@ lemma distLaplacian_distOfFunction_norm_zpow {d : ℕ} [NeZero d] (m : ℤ) (IsDistBounded.zpow_smul_repr_self (m - 2) (by omega)) (m : ℝ) using 1 ext x simp [smul_smul] - rw [hdist] - rw [map_smul] - rw [distDiv_norm_zpow_smul_repr_self_eq_smul (m - 2) hdiv] - rw [smul_smul] + rw [hdist, map_smul, distDiv_norm_zpow_smul_repr_self_eq_smul (m - 2) hdiv, smul_smul] /-! @@ -1287,8 +993,7 @@ lemma distDiv_inv_pow_eq_dim {d : ℕ} [NeZero d] : simp only [Real.norm_eq_abs, inv_pow, Function.comp_apply, homeomorphUnitSphereProd_symm_apply_coe, map_smul] let x : Space d := r.2.1 • r.1.1 - have hr := r.2.2 - simp [-Subtype.coe_prop] at hr + have hr : (0 : ℝ) < r.2.1 := r.2.2 rw [abs_of_nonneg (le_of_lt hr)] trans (r.2.1 ^ (d - 1))⁻¹ * _root_.deriv (fun a => η (a • ‖↑x‖⁻¹ • ↑x)) ‖x‖ · simp [x, norm_smul] @@ -1316,8 +1021,7 @@ lemma distDiv_inv_pow_eq_dim {d : ℕ} [NeZero d] : erw [integral_withDensity_eq_integral_smul] congr funext r - have hr := r.2 - simp [-Subtype.coe_prop] at hr + have hr : (0 : ℝ) < r.1 := r.2 rw [abs_of_nonneg hr.le, NNReal.smul_def, Real.coe_toNNReal _ (by positivity), smul_eq_mul, ← mul_assoc, mul_inv_cancel₀ (pow_ne_zero (d - 1) hr.ne'), one_mul] fun_prop @@ -1349,12 +1053,8 @@ lemma distDiv_inv_pow_eq_dim {d : ℕ} [NeZero d] : rw [MeasureTheory.integral_subtype_comap (by simp), MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto (f := fun a => η (a • n)) (m := 0)] · simp - · refine ContinuousAt.continuousWithinAt ?_ - fun_prop - · intro x hx - refine DifferentiableAt.hasDerivAt ?_ - have := η.differentiable - fun_prop + · exact ContinuousAt.continuousWithinAt (by fun_prop) + · exact fun x _ => DifferentiableAt.hasDerivAt (by fun_prop) · exact (integrable ((derivCLM ℝ ℝ) (η' n))).integrableOn · exact Filter.Tendsto.mono_left (η' n).toZeroAtInfty.zero_at_infty' atTop_le_cocompact _ = η 0 * (d * (volume (α := Space d)).real (Metric.ball 0 1)) := by @@ -1390,9 +1090,7 @@ lemma distLaplacian_fundamentalSolution_norm_zpow {d : ℕ} : rw [distOfFunction_apply] refine integral_eq_zero_of_ae (ae_of_all _ fun x => ?_) rw [Subsingleton.elim x 0] - simp only [norm_zero, smul_eq_mul, Pi.zero_apply, mul_eq_zero] - right - linarith + simp [zero_zpow_eq] simp [hzero] · haveI : NeZero d := ⟨by omega⟩ rw [distLaplacian] @@ -1422,17 +1120,7 @@ lemma distLaplacian_fundamentalSolution_norm_zpow {d : ℕ} : (2 - (d : ℝ)) using 1 ext x simp [smul_smul] - rw [hdist] - rw [map_smul] - have hdiv : - ∇ᵈ ⬝ (distOfFunction - (fun x : Space d => - ‖x‖ ^ (- (d : ℤ)) • basis.repr x) - (IsDistBounded.zpow_smul_repr_self (- (d : ℤ)) (by omega))) = - (d * (volume (α := Space d)).real - (Metric.ball 0 1)) • diracDelta ℝ 0 := distDiv_inv_pow_eq_dim (d := d) - rw [hdiv] - rw [smul_smul] + rw [hdist, map_smul, distDiv_inv_pow_eq_dim, smul_smul] ring_nf /-- In dimension two the fundamental solution of the Laplacian is the logarithm: the From de8ef935316ac9d757efd0e9f734bee61e68252f Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Fri, 3 Jul 2026 21:50:39 -0700 Subject: [PATCH 2/3] refactor: golf Wick contraction insert/sign proofs Golf proof bodies in WickContraction/InsertAndContractNat and Sign/InsertSome: reuse erase_insert and getDualErase lemmas, replace manual Fin.succAbove case bashes with omega fed the relevant order couplings. Statements unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3 --- .../WickContraction/InsertAndContractNat.lean | 545 ++++------------ .../WickContraction/Sign/InsertSome.lean | 580 +++--------------- 2 files changed, 203 insertions(+), 922 deletions(-) diff --git a/Physlib/QFT/PerturbationTheory/WickContraction/InsertAndContractNat.lean b/Physlib/QFT/PerturbationTheory/WickContraction/InsertAndContractNat.lean index e6a45f574..9cd92d5a6 100644 --- a/Physlib/QFT/PerturbationTheory/WickContraction/InsertAndContractNat.lean +++ b/Physlib/QFT/PerturbationTheory/WickContraction/InsertAndContractNat.lean @@ -129,31 +129,14 @@ lemma insertAndContractNat_of_isSome (c : WickContraction n) (i : Fin n.succ) (j : Option c.uncontracted) (hj : j.isSome) : (insertAndContractNat c i j).1 = Insert.insert {i, i.succAbove (j.get hj)} (Finset.map (Finset.mapEmbedding i.succAboveEmb).toEmbedding c.1) := by - simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset] - rw [@Option.isSome_iff_exists] at hj - obtain ⟨j, hj⟩ := hj - subst hj - simp + obtain ⟨j, rfl⟩ := Option.isSome_iff_exists.mp hj + simp [insertAndContractNat] @[simp] lemma self_mem_uncontracted_of_insertAndContractNat_none (c : WickContraction n) (i : Fin n.succ) : i ∈ (insertAndContractNat c i none).uncontracted := by - rw [mem_uncontracted_iff_not_contracted] - intro p hp - simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, Finset.mem_map, - RelEmbedding.coe_toEmbedding] at hp - obtain ⟨a, ha, ha'⟩ := hp - have hc := c.2.1 a ha - rw [@Finset.card_eq_two] at hc - obtain ⟨x, y, hxy, ha⟩ := hc - subst ha - subst ha' - rw [Finset.mapEmbedding_apply] - simp only [Nat.succ_eq_add_one, Finset.map_insert, Fin.succAboveEmb_apply, Finset.map_singleton, - Finset.mem_insert, Finset.mem_singleton, not_or] - apply And.intro - · exact Fin.ne_succAbove i x - · exact Fin.ne_succAbove i y + simp [mem_uncontracted_iff_not_contracted, insertAndContractNat, Finset.mapEmbedding_apply, + Fin.succAbove_ne, -Finset.le_eq_subset] @[simp] lemma self_not_mem_uncontracted_of_insertAndContractNat_some (c : WickContraction n) @@ -164,146 +147,32 @@ lemma self_not_mem_uncontracted_of_insertAndContractNat_some (c : WickContractio lemma insertAndContractNat_succAbove_mem_uncontracted_iff (c : WickContraction n) (i : Fin n.succ) (j : Fin n) : (i.succAbove j) ∈ (insertAndContractNat c i none).uncontracted ↔ j ∈ c.uncontracted := by - rw [mem_uncontracted_iff_not_contracted, mem_uncontracted_iff_not_contracted] - simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, Finset.mem_map, - RelEmbedding.coe_toEmbedding, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] - apply Iff.intro - · intro h p hp - have hp' := h p hp - have hc := c.2.1 p hp - rw [Finset.card_eq_two] at hc - obtain ⟨x, y, hxy, hp⟩ := hc - subst hp - rw [Finset.mapEmbedding_apply] at hp' - simp only [Finset.map_insert, Fin.succAboveEmb_apply, Finset.map_singleton, Finset.mem_insert, - Finset.mem_singleton, not_or] at hp' - simp only [Finset.mem_insert, Finset.mem_singleton, not_or] - exact And.intro (fun a => hp'.1 (congrArg i.succAbove a)) - (fun a => hp'.2 (congrArg i.succAbove a)) - · intro h p hp - have hc := c.2.1 p hp - rw [Finset.card_eq_two] at hc - obtain ⟨x, y, hxy, hp⟩ := hc - subst hp - rw [Finset.mapEmbedding_apply] - simp only [Finset.map_insert, Fin.succAboveEmb_apply, Finset.map_singleton, Finset.mem_insert, - Finset.mem_singleton, not_or] - have hp' := h {x, y} hp - simp only [Finset.mem_insert, Finset.mem_singleton, not_or] at hp' - apply And.intro - (fun a => hp'.1 (i.succAbove_right_injective a)) - (fun a => hp'.2 (i.succAbove_right_injective a)) + simp [mem_uncontracted_iff_not_contracted, insertAndContractNat, Finset.mapEmbedding_apply, + -Finset.le_eq_subset] @[simp] lemma mem_uncontracted_insertAndContractNat_none_iff (c : WickContraction n) (i : Fin n.succ) (k : Fin n.succ) : k ∈ (insertAndContractNat c i none).uncontracted ↔ k = i ∨ ∃ j, k = i.succAbove j ∧ j ∈ c.uncontracted := by - by_cases hi : k = i - · subst hi - simp - · simp only [Nat.succ_eq_add_one, ← Fin.exists_succAbove_eq_iff] at hi - obtain ⟨z, hk⟩ := hi - subst hk - have hn : ¬ i.succAbove z = i := Fin.succAbove_ne i z - simp only [Nat.succ_eq_add_one, insertAndContractNat_succAbove_mem_uncontracted_iff, hn, - false_or] - apply Iff.intro - · intro h - exact ⟨z, rfl, h⟩ - · intro h - obtain ⟨j, hk⟩ := h - have hjk : z = j := Fin.succAbove_right_inj.mp hk.1 - subst hjk - exact hk.2 + rcases Fin.eq_self_or_eq_succAbove i k with rfl | ⟨z, rfl⟩ + · simp + · simp [insertAndContractNat_succAbove_mem_uncontracted_iff, Fin.succAbove_ne] lemma insertAndContractNat_none_uncontracted (c : WickContraction n) (i : Fin n.succ) : (insertAndContractNat c i none).uncontracted = Insert.insert i (c.uncontracted.map i.succAboveEmb) := by ext a - simp only [Nat.succ_eq_add_one, mem_uncontracted_insertAndContractNat_none_iff, Finset.mem_insert, - Finset.mem_map, Fin.succAboveEmb_apply] - apply Iff.intro - · intro a_1 - cases a_1 with - | inl h => - subst h - simp_all only [true_or] - | inr h_1 => - obtain ⟨w, h⟩ := h_1 - obtain ⟨left, right⟩ := h - subst left - apply Or.inr - apply Exists.intro - · apply And.intro - on_goal 2 => {rfl - } - · simp_all only - · intro a_1 - cases a_1 with - | inl h => - subst h - simp_all only [true_or] - | inr h_1 => - obtain ⟨w, h⟩ := h_1 - obtain ⟨left, right⟩ := h - subst right - apply Or.inr - apply Exists.intro - · apply And.intro - on_goal 2 => {exact left - } - · simp_all only + simp [mem_uncontracted_insertAndContractNat_none_iff, and_comm, eq_comm] @[simp] lemma mem_uncontracted_insertAndContractNat_some_iff (c : WickContraction n) (i : Fin n.succ) (k : Fin n.succ) (j : c.uncontracted) : k ∈ (insertAndContractNat c i (some j)).uncontracted ↔ ∃ z, k = i.succAbove z ∧ z ∈ c.uncontracted ∧ z ≠ j := by - by_cases hki : k = i - · subst hki - simp only [Nat.succ_eq_add_one, self_not_mem_uncontracted_of_insertAndContractNat_some, ne_eq, - false_iff, not_exists, not_and, Decidable.not_not] - exact fun x hx => False.elim (Fin.ne_succAbove k x hx) - · simp only [Nat.succ_eq_add_one, ← Fin.exists_succAbove_eq_iff] at hki - obtain ⟨z, hk⟩ := hki - subst hk - by_cases hjz : j = z - · subst hjz - rw [mem_uncontracted_iff_not_contracted] - simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, Finset.mem_insert, - Finset.mem_map, RelEmbedding.coe_toEmbedding, forall_eq_or_imp, Finset.mem_singleton, - or_true, not_true_eq_false, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, - false_and, ne_eq, false_iff, not_exists, not_and, Decidable.not_not] - intro x - rw [Function.Injective.eq_iff (Fin.succAbove_right_injective)] - exact fun a _a => a.symm - · apply Iff.intro - · intro h - use z - simp only [Nat.succ_eq_add_one, ne_eq, true_and] - refine And.intro ?_ (fun a => hjz a.symm) - rw [mem_uncontracted_iff_not_contracted] - intro p hp - rw [mem_uncontracted_iff_not_contracted] at h - simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, - Finset.mem_insert, Finset.mem_map, RelEmbedding.coe_toEmbedding, forall_eq_or_imp, - Finset.mem_singleton, not_or, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at h - have hc := h.2 p hp - rw [Finset.mapEmbedding_apply] at hc - exact (Finset.mem_map' (i.succAboveEmb)).mpr.mt hc - · intro h - obtain ⟨z', hz'1, hz'⟩ := h - rw [Function.Injective.eq_iff (Fin.succAbove_right_injective)] at hz'1 - subst hz'1 - rw [mem_uncontracted_iff_not_contracted] - simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, - Finset.mem_insert, Finset.mem_map, RelEmbedding.coe_toEmbedding, forall_eq_or_imp, - Finset.mem_singleton, not_or, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] - apply And.intro - · rw [Function.Injective.eq_iff (Fin.succAbove_right_injective)] - exact And.intro (Fin.succAbove_ne i z) (fun a => hjz a.symm) - · rw [mem_uncontracted_iff_not_contracted] at hz' - exact fun a ha hc => hz'.1 a ha ((Finset.mem_map' (i.succAboveEmb)).mp hc) + rcases Fin.eq_self_or_eq_succAbove i k with rfl | ⟨z, rfl⟩ + · simp [Fin.ne_succAbove] + · simp [insertAndContractNat, mem_uncontracted_iff_not_contracted, Fin.succAbove_ne, + Finset.mapEmbedding_apply, and_comm, -Finset.le_eq_subset] lemma insertAndContractNat_some_uncontracted (c : WickContraction n) (i : Fin n.succ) (j : c.uncontracted) : @@ -312,24 +181,7 @@ lemma insertAndContractNat_some_uncontracted (c : WickContraction n) (i : Fin n. ext a simp only [Nat.succ_eq_add_one, mem_uncontracted_insertAndContractNat_some_iff, ne_eq, Finset.map_erase, Fin.succAboveEmb_apply, Finset.mem_erase, Finset.mem_map] - apply Iff.intro - · intro h - obtain ⟨z, h1, h2, h3⟩ := h - subst h1 - rw [Function.Injective.eq_iff (Fin.succAbove_right_injective)] - simp only [h3, not_false_eq_true, true_and] - use z - · intro h - obtain ⟨z, h1, h2⟩ := h.2 - use z - subst h2 - simp only [true_and] - obtain ⟨a, ha1, ha2⟩ := h.2 - rw [Function.Injective.eq_iff (Fin.succAbove_right_injective)] at ha2 - subst ha2 - simp_all only [true_and] - rw [Function.Injective.eq_iff (Fin.succAbove_right_injective)] at h - exact h.1 + grind [Fin.succAbove_right_inj] /-! @@ -340,47 +192,36 @@ lemma insertAndContractNat_some_uncontracted (c : WickContraction n) (i : Fin n. set_option backward.isDefEq.respectTransparency false in lemma insertAndContractNat_none_getDual?_isNone (c : WickContraction n) (i : Fin n.succ) : ((insertAndContractNat c i none).getDual? i).isNone := by - have hi : i ∈ (insertAndContractNat c i none).uncontracted := by simp - simp only [Nat.succ_eq_add_one, uncontracted, Finset.mem_filter, Finset.mem_univ, true_and] at hi - simp [hi] + simp [Option.isNone_iff_eq_none, getDual?_eq_none_iff_mem_uncontracted] set_option backward.isDefEq.respectTransparency false in @[simp] lemma insertAndContractNat_none_getDual?_eq_none (c : WickContraction n) (i : Fin n.succ) : (insertAndContractNat c i none).getDual? i = none := by - have hi : i ∈ (insertAndContractNat c i none).uncontracted := by simp - simp only [Nat.succ_eq_add_one, uncontracted, Finset.mem_filter, Finset.mem_univ, true_and] at hi - rw [hi] + simp [getDual?_eq_none_iff_mem_uncontracted] @[simp] lemma insertAndContractNat_succAbove_getDual?_eq_none_iff (c : WickContraction n) (i : Fin n.succ) (j : Fin n) : (insertAndContractNat c i none).getDual? (i.succAbove j) = none ↔ c.getDual? j = none := by - have h1 := insertAndContractNat_succAbove_mem_uncontracted_iff c i j - simpa [uncontracted] using h1 + simpa [uncontracted] using insertAndContractNat_succAbove_mem_uncontracted_iff c i j @[simp] lemma insertAndContractNat_succAbove_getDual?_isSome_iff (c : WickContraction n) (i : Fin n.succ) (j : Fin n) : ((insertAndContractNat c i none).getDual? (i.succAbove j)).isSome ↔ (c.getDual? j).isSome := by - rw [← not_iff_not] - simp + simp [Option.isSome_iff_ne_none] @[simp] lemma insertAndContractNat_succAbove_getDual?_get (c : WickContraction n) (i : Fin n.succ) (j : Fin n) (h : ((insertAndContractNat c i none).getDual? (i.succAbove j)).isSome) : ((insertAndContractNat c i none).getDual? (i.succAbove j)).get h = i.succAbove ((c.getDual? j).get (by simpa using h)) := by - have h1 : (insertAndContractNat c i none).getDual? (i.succAbove j) = some - (i.succAbove ((c.getDual? j).get (by simpa using h))) := by - rw [getDual?_eq_some_iff_mem] - simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, Finset.mem_map, - RelEmbedding.coe_toEmbedding] - use {j, ((c.getDual? j).get (by simpa using h))} - simp only [self_getDual?_get_mem, true_and] - rw [Finset.mapEmbedding_apply] - simp - exact Option.get_of_mem h h1 + refine Option.get_of_mem h ((getDual?_eq_some_iff_mem _ _ _).mpr ?_) + simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.mem_map, + RelEmbedding.coe_toEmbedding] + exact ⟨_, self_getDual?_get_mem c j (by simpa using h), + by simp [Finset.mapEmbedding_apply, -Finset.le_eq_subset]⟩ @[simp] lemma insertAndContractNat_some_getDual?_eq (c : WickContraction n) (i : Fin n.succ) @@ -391,30 +232,13 @@ lemma insertAndContractNat_some_getDual?_eq (c : WickContraction n) (i : Fin n.s lemma insertAndContractNat_some_getDual?_ne_none (c : WickContraction n) (i : Fin n.succ) (j : c.uncontracted) (k : Fin n) (hkj : k ≠ j.1) : (insertAndContractNat c i (some j)).getDual? (i.succAbove k) = none ↔ c.getDual? k = none := by - apply Iff.intro - · intro h - have hk : (i.succAbove k) ∈ (insertAndContractNat c i (some j)).uncontracted := by - simp only [Nat.succ_eq_add_one, uncontracted, Finset.mem_filter, Finset.mem_univ, true_and] - exact h - simp only [Nat.succ_eq_add_one, mem_uncontracted_insertAndContractNat_some_iff, ne_eq] at hk - obtain ⟨z, hz1, hz2, hz3⟩ := hk - rw [Function.Injective.eq_iff (Fin.succAbove_right_injective)] at hz1 - subst hz1 - simpa [uncontracted] using hz2 - · intro h - have hk : (i.succAbove k) ∈ (insertAndContractNat c i (some j)).uncontracted := by - simp only [Nat.succ_eq_add_one, mem_uncontracted_insertAndContractNat_some_iff, ne_eq] - use k - simp only [hkj, not_false_eq_true, and_true, true_and] - simpa [uncontracted] using h - simpa [uncontracted, -mem_uncontracted_insertAndContractNat_some_iff, ne_eq] using hk + simp [getDual?_eq_none_iff_mem_uncontracted, hkj] lemma insertAndContractNat_some_getDual?_ne_isSome (c : WickContraction n) (i : Fin n.succ) (j : c.uncontracted) (k : Fin n) (hkj : k ≠ j.1) : ((insertAndContractNat c i (some j)).getDual? (i.succAbove k)).isSome ↔ (c.getDual? k).isSome := by - rw [← not_iff_not] - simp [hkj, insertAndContractNat_some_getDual?_ne_none] + simp [Option.isSome_iff_ne_none, insertAndContractNat_some_getDual?_ne_none c i j k hkj] lemma insertAndContractNat_some_getDual?_ne_isSome_get (c : WickContraction n) (i : Fin n.succ) (j : c.uncontracted) (k : Fin n) (hkj : k ≠ j.1) @@ -422,40 +246,25 @@ lemma insertAndContractNat_some_getDual?_ne_isSome_get (c : WickContraction n) ( ((insertAndContractNat c i (some j)).getDual? (i.succAbove k)).get h = i.succAbove ((c.getDual? k).get (by simpa [hkj, insertAndContractNat_some_getDual?_ne_isSome] using h)) := by - have h1 : ((insertAndContractNat c i (some j)).getDual? (i.succAbove k)) - = some (i.succAbove ((c.getDual? k).get - (by simpa [hkj, insertAndContractNat_some_getDual?_ne_isSome] using h))) := by - rw [getDual?_eq_some_iff_mem] - simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, Finset.mem_insert, - Finset.mem_map, RelEmbedding.coe_toEmbedding] - apply Or.inr - use { k, ((c.getDual? k).get - (by simpa [hkj, insertAndContractNat_some_getDual?_ne_isSome] using h))} - simp only [self_getDual?_get_mem, true_and] - rw [Finset.mapEmbedding_apply] - simp - exact Option.get_of_mem h h1 + refine Option.get_of_mem h ((getDual?_eq_some_iff_mem _ _ _).mpr ?_) + simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.mem_insert, + Finset.mem_map, RelEmbedding.coe_toEmbedding] + exact Or.inr ⟨_, self_getDual?_get_mem c k + (by simpa [hkj, insertAndContractNat_some_getDual?_ne_isSome] using h), + by simp [Finset.mapEmbedding_apply, -Finset.le_eq_subset]⟩ @[simp] lemma insertAndContractNat_some_getDual?_of_neq (c : WickContraction n) (i : Fin n.succ) (j : c.uncontracted) (k : Fin n) (hkj : k ≠ j.1) : (insertAndContractNat c i (some j)).getDual? (i.succAbove k) = Option.map i.succAbove (c.getDual? k) := by - by_cases h : (c.getDual? k).isSome - · have h1 : (c.insertAndContractNat i (some j)).getDual? (i.succAbove k) = - some (i.succAbove ((c.getDual? k).get h)) := by - rw [← insertAndContractNat_some_getDual?_ne_isSome_get c i j k hkj] - refine Eq.symm (Option.some_get ?_) - all_goals - simpa [hkj, insertAndContractNat_some_getDual?_ne_isSome] using h - rw [h1] - have h2 :(c.getDual? k) = some ((c.getDual? k).get h) := by simp - conv_rhs => rw [h2] - rw [@Option.map_coe'] - · simp only [Bool.not_eq_true, Option.isSome_eq_false_iff, Option.isNone_iff_eq_none] at h - simp only [Nat.succ_eq_add_one, h, Option.map_none] - simp only [ne_eq, hkj, not_false_eq_true, insertAndContractNat_some_getDual?_ne_none] - exact h + rcases hc : c.getDual? k with _ | d + · simp [hc, insertAndContractNat_some_getDual?_ne_none c i j k hkj] + · rw [Option.map_some, getDual?_eq_some_iff_mem] + simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.mem_insert, + Finset.mem_map, RelEmbedding.coe_toEmbedding] + exact Or.inr ⟨{k, d}, (c.getDual?_eq_some_iff_mem k d).mp hc, + by simp [Finset.mapEmbedding_apply, -Finset.le_eq_subset]⟩ /-! @@ -466,47 +275,17 @@ lemma insertAndContractNat_some_getDual?_of_neq (c : WickContraction n) (i : Fin @[simp] lemma insertAndContractNat_erase (c : WickContraction n) (i : Fin n.succ) (j : Option c.uncontracted) : erase (insertAndContractNat c i j) i = c := by - refine Subtype.ext ?_ - simp only [erase, Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset] - conv_rhs => rw [c.eq_filter_mem_self] - refine Finset.filter_inj'.mpr ?_ - intro a _ + refine Subtype.ext (Finset.ext fun a => ?_) + simp only [erase, Nat.succ_eq_add_one, insertAndContractNat, Finset.mem_filter, Finset.mem_univ, + true_and] match j with | none => - simp only [Finset.mem_map, RelEmbedding.coe_toEmbedding] - apply Iff.intro - · intro ha - obtain ⟨a', ha', ha''⟩ := ha - rw [Finset.mapEmbedding_apply] at ha'' - simp only [Finset.map_inj] at ha'' - subst ha'' - exact ha' - · intro ha - use a - simp only [ha, true_and] - rw [Finset.mapEmbedding_apply] + simp [Finset.mapEmbedding_apply, Finset.map_inj, -Finset.le_eq_subset] | some j => - simp only [Finset.mem_insert, Finset.mem_map, RelEmbedding.coe_toEmbedding] - apply Iff.intro - · intro ha - rcases ha with ha | ha - · have hin : ¬ i ∈ Finset.map i.succAboveEmb a := by - simp only [Nat.succ_eq_add_one, Finset.mem_map, Fin.succAboveEmb_apply, not_exists, - not_and] - intro x - exact fun a => Fin.succAbove_ne i x - refine False.elim (hin ?_) - simp [ha] - · obtain ⟨a', ha', ha''⟩ := ha - rw [Finset.mapEmbedding_apply] at ha'' - simp only [Finset.map_inj] at ha'' - subst ha'' - exact ha' - · intro ha - apply Or.inr - use a - simp only [ha, true_and] - rw [Finset.mapEmbedding_apply] + have hn : Finset.map i.succAboveEmb a ≠ {i, i.succAbove j} := fun h => by + have hi : i ∈ Finset.map i.succAboveEmb a := h ▸ Finset.mem_insert_self i _ + simp [Fin.succAbove_ne] at hi + simp [Finset.mapEmbedding_apply, Finset.map_inj, hn, -Finset.le_eq_subset] set_option backward.isDefEq.respectTransparency false in lemma insertAndContractNat_getDualErase (c : WickContraction n) (i : Fin n.succ) @@ -514,18 +293,14 @@ lemma insertAndContractNat_getDualErase (c : WickContraction n) (i : Fin n.succ) uncontractedCongr (c := c) (c' := (c.insertAndContractNat i j).erase i) (by simp) j := by match n with | 0 => - simp only [insertAndContractNat, Nat.succ_eq_add_one, Nat.reduceAdd, Finset.le_eq_subset, - getDualErase] fin_cases j - simp + simp [getDualErase] | Nat.succ n => match j with | none => simp [getDualErase] | some j => - simp only [Nat.succ_eq_add_one, getDualErase, insertAndContractNat_some_getDual?_eq, - Option.isSome_some, ↓reduceDIte, Option.get_some, predAboveI_succAbove, - uncontractedCongr_some, Option.some.injEq] + simp [getDualErase] rfl @[simp] @@ -538,23 +313,12 @@ lemma erase_insert (c : WickContraction n.succ) (i : Fin n.succ) : Finset.le_eq_subset] ext a simp only [Finset.mem_map, RelEmbedding.coe_toEmbedding] - apply Iff.intro - · intro h - simp only [erase, Nat.reduceAdd, Nat.succ_eq_add_one, Finset.mem_filter, Finset.mem_univ, - true_and] at h - obtain ⟨a', ha', ha''⟩ := h - subst ha'' - exact ha' + constructor + · rintro ⟨a', ha', rfl⟩ + exact (Finset.mem_filter.mp ha').2 · intro ha - obtain ⟨a, ha⟩ := c.mem_not_eq_erase_of_isNone (a := a) i (by simp) ha - simp_all only [Nat.succ_eq_add_one] - obtain ⟨left, right⟩ := ha - subst right - apply Exists.intro - · apply And.intro - on_goal 2 => {rfl - } - · simp_all only + obtain ⟨a', ha', rfl⟩ := c.mem_not_eq_erase_of_isNone (a := a) i (by simp) ha + exact ⟨a', ha', rfl⟩ | Nat.succ n => apply Subtype.ext by_cases hi : (c.getDual? i).isSome @@ -562,52 +326,29 @@ lemma erase_insert (c : WickContraction n.succ) (i : Fin n.succ) : simp only [Nat.succ_eq_add_one, getDualErase, hi, ↓reduceDIte, Option.get_some, Finset.le_eq_subset] rw [succsAbove_predAboveI] - ext a - apply Iff.intro - · simp only [Finset.mem_insert, Finset.mem_map, RelEmbedding.coe_toEmbedding] - intro ha - rcases ha with ha | ha - · subst ha - simp - · obtain ⟨a', ha', ha''⟩ := ha - subst ha'' - simp_all only [Nat.succ_eq_add_one, erase, Finset.mem_filter, Finset.mem_univ, true_and] - exact ha' - · intro ha + · ext a simp only [Finset.mem_insert, Finset.mem_map, RelEmbedding.coe_toEmbedding] - by_cases hia : a = {i, (c.getDual? i).get hi} - · subst hia - simp - · apply Or.inr - simp only [erase, Nat.succ_eq_add_one, Finset.mem_filter, Finset.mem_univ, true_and] - obtain ⟨a', ha'⟩ := c.mem_not_eq_erase_of_isSome (a := a) i hi ha hia - use a' - simp_all only [Nat.succ_eq_add_one, true_and] - obtain ⟨left, right⟩ := ha' - subst right - rfl - simp only [Nat.succ_eq_add_one, ne_eq, self_ne_getDual?_get, not_false_eq_true] - exact (getDualErase_isSome_iff_getDual?_isSome c i).mpr hi + constructor + · rintro (rfl | ⟨a', ha', rfl⟩) + · simp + · exact (Finset.mem_filter.mp ha').2 + · intro ha + by_cases hia : a = {i, (c.getDual? i).get hi} + · exact Or.inl hia + · obtain ⟨a', ha', rfl⟩ := c.mem_not_eq_erase_of_isSome (a := a) i hi ha hia + exact Or.inr ⟨a', ha', rfl⟩ + · simp + · exact (getDualErase_isSome_iff_getDual?_isSome c i).mpr hi · simp only [Nat.succ_eq_add_one, insertAndContractNat, getDualErase, hi, Bool.false_eq_true, ↓reduceDIte, Finset.le_eq_subset] ext a simp only [Finset.mem_map, RelEmbedding.coe_toEmbedding] - apply Iff.intro - · intro h - simp only [erase, Nat.succ_eq_add_one, Finset.mem_filter, Finset.mem_univ, true_and] at h - obtain ⟨a', ha', ha''⟩ := h - subst ha'' - exact ha' + constructor + · rintro ⟨a', ha', rfl⟩ + exact (Finset.mem_filter.mp ha').2 · intro ha - obtain ⟨a, ha⟩ := c.mem_not_eq_erase_of_isNone (a := a) i (by simpa using hi) ha - simp_all only [Nat.succ_eq_add_one, Bool.not_eq_true] - obtain ⟨left, right⟩ := ha - subst right - apply Exists.intro - · apply And.intro - on_goal 2 => {rfl - } - · simp_all only + obtain ⟨a', ha', rfl⟩ := c.mem_not_eq_erase_of_isNone (a := a) i (by simpa using hi) ha + exact ⟨a', ha', rfl⟩ /-- Lifts a contraction in `c` to a contraction in `(c.insert i j)`. -/ def insertLift {c : WickContraction n} (i : Fin n.succ) (j : Option (c.uncontracted)) @@ -627,54 +368,40 @@ def insertLift {c : WickContraction n} (i : Fin n.succ) (j : Option (c.uncontrac rfl⟩ lemma insertLift_injective {c : WickContraction n} (i : Fin n.succ) (j : Option (c.uncontracted)) : - Function.Injective (insertLift i j) := by - intro a b hab - simp only [Nat.succ_eq_add_one, insertLift, Subtype.mk.injEq, Finset.map_inj] at hab - exact Subtype.ext hab + Function.Injective (insertLift i j) := fun _ _ hab => + Subtype.ext (Finset.map_injective _ (Subtype.ext_iff.mp hab)) lemma insertLift_none_surjective {c : WickContraction n} (i : Fin n.succ) : Function.Surjective (c.insertLift i none) := by intro a - have ha := a.2 - simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, Finset.mem_map, - RelEmbedding.coe_toEmbedding] at ha - obtain ⟨a', ha', ha''⟩ := ha - use ⟨a', ha'⟩ - exact Subtype.ext ha'' + obtain ⟨a', ha', ha''⟩ := Finset.mem_map.mp a.2 + exact ⟨⟨a', ha'⟩, Subtype.ext ha''⟩ lemma insertLift_none_bijective {c : WickContraction n} (i : Fin n.succ) : - Function.Bijective (c.insertLift i none) := by - exact ⟨insertLift_injective i none, insertLift_none_surjective i⟩ + Function.Bijective (c.insertLift i none) := + ⟨insertLift_injective i none, insertLift_none_surjective i⟩ @[simp] lemma insertAndContractNat_fstFieldOfContract (c : WickContraction n) (i : Fin n.succ) (j : Option (c.uncontracted)) (a : c.1) : (c.insertAndContractNat i j).fstFieldOfContract (insertLift i j a) = - i.succAbove (c.fstFieldOfContract a) := by - refine (c.insertAndContractNat i j).eq_fstFieldOfContract_of_mem (a := (insertLift i j a)) - (i := i.succAbove (c.fstFieldOfContract a)) (j := i.succAbove (c.sndFieldOfContract a)) ?_ ?_ ?_ - · simp only [Nat.succ_eq_add_one, insertLift, Finset.mem_map, Fin.succAboveEmb_apply] - use (c.fstFieldOfContract a) - simp - · simp only [Nat.succ_eq_add_one, insertLift, Finset.mem_map, Fin.succAboveEmb_apply] - use (c.sndFieldOfContract a) - simp - · exact Fin.succAbove_lt_succAbove_iff.mpr (fstFieldOfContract_lt_sndFieldOfContract c a) + i.succAbove (c.fstFieldOfContract a) := + (c.insertAndContractNat i j).eq_fstFieldOfContract_of_mem (insertLift i j a) + (i.succAbove (c.fstFieldOfContract a)) (i.succAbove (c.sndFieldOfContract a)) + (Finset.mem_map_of_mem _ (fstFieldOfContract_mem c a)) + (Finset.mem_map_of_mem _ (sndFieldOfContract_mem c a)) + (Fin.succAbove_lt_succAbove_iff.mpr (fstFieldOfContract_lt_sndFieldOfContract c a)) @[simp] lemma insertAndContractNat_sndFieldOfContract (c : WickContraction n) (i : Fin n.succ) (j : Option (c.uncontracted)) (a : c.1) : (c.insertAndContractNat i j).sndFieldOfContract (insertLift i j a) = - i.succAbove (c.sndFieldOfContract a) := by - refine (c.insertAndContractNat i j).eq_sndFieldOfContract_of_mem (a := (insertLift i j a)) - (i := i.succAbove (c.fstFieldOfContract a)) (j := i.succAbove (c.sndFieldOfContract a)) ?_ ?_ ?_ - · simp only [Nat.succ_eq_add_one, insertLift, Finset.mem_map, Fin.succAboveEmb_apply] - use (c.fstFieldOfContract a) - simp - · simp only [Nat.succ_eq_add_one, insertLift, Finset.mem_map, Fin.succAboveEmb_apply] - use (c.sndFieldOfContract a) - simp - · exact Fin.succAbove_lt_succAbove_iff.mpr (fstFieldOfContract_lt_sndFieldOfContract c a) + i.succAbove (c.sndFieldOfContract a) := + (c.insertAndContractNat i j).eq_sndFieldOfContract_of_mem (insertLift i j a) + (i.succAbove (c.fstFieldOfContract a)) (i.succAbove (c.sndFieldOfContract a)) + (Finset.mem_map_of_mem _ (fstFieldOfContract_mem c a)) + (Finset.mem_map_of_mem _ (sndFieldOfContract_mem c a)) + (Fin.succAbove_lt_succAbove_iff.mpr (fstFieldOfContract_lt_sndFieldOfContract c a)) /-- Given a contracted pair for a Wick contraction `WickContraction n`, the corresponding contracted pair of a wick contraction `(c.insert i (some j))` formed @@ -691,45 +418,20 @@ lemma insertLiftSome_injective {c : WickContraction n} (i : Fin n.succ) (j : c.u intro a b hab match a, b with | Sum.inl (), Sum.inl () => rfl - | Sum.inl (), Sum.inr a => + | Sum.inl (), Sum.inr a | Sum.inr a, Sum.inl () => simp only [Nat.succ_eq_add_one, insertLiftSome, insertLift, Subtype.mk.injEq] at hab - rw [finset_eq_fstFieldOfContract_sndFieldOfContract] at hab - simp only [Finset.map_insert, Fin.succAboveEmb_apply, Finset.map_singleton] at hab - have hi : i ∈ ({i.succAbove (c.fstFieldOfContract a), - i.succAbove (c.sndFieldOfContract a)} : Finset (Fin (n + 1))) := by - simp [← hab] - simp only [Nat.succ_eq_add_one, Finset.mem_insert, Finset.mem_singleton] at hi - rcases hi with hi | hi - · exact False.elim (Fin.ne_succAbove _ _ hi) - · exact False.elim (Fin.ne_succAbove _ _ hi) - | Sum.inr a, Sum.inl () => - simp only [Nat.succ_eq_add_one, insertLiftSome, insertLift, Subtype.mk.injEq] at hab - rw [finset_eq_fstFieldOfContract_sndFieldOfContract] at hab - simp only [Finset.map_insert, Fin.succAboveEmb_apply, Finset.map_singleton] at hab - have hi : i ∈ ({i.succAbove (c.fstFieldOfContract a), - i.succAbove (c.sndFieldOfContract a)} : Finset (Fin (n + 1))) := by - simp [hab] - simp only [Nat.succ_eq_add_one, Finset.mem_insert, Finset.mem_singleton] at hi - rcases hi with hi | hi - · exact False.elim (Fin.ne_succAbove _ _ hi) - · exact False.elim (Fin.ne_succAbove _ _ hi) + have hi : i ∈ Finset.map (Fin.succAboveEmb i) a.1 := hab ▸ Finset.mem_insert_self i _ + simp [Fin.succAbove_ne] at hi | Sum.inr a, Sum.inr b => - simp only [Nat.succ_eq_add_one, insertLiftSome] at hab - simpa using insertLift_injective i (some j) hab + exact congrArg Sum.inr (insertLift_injective i (some j) hab) lemma insertLiftSome_surjective {c : WickContraction n} (i : Fin n.succ) (j : c.uncontracted) : Function.Surjective (insertLiftSome i j) := by intro a - have ha := a.2 - simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, Finset.mem_insert, - Finset.mem_map, RelEmbedding.coe_toEmbedding] at ha - rcases ha with ha | ha - · use Sum.inl () - exact Subtype.ext ha.symm - · obtain ⟨a', ha', ha''⟩ := ha - use Sum.inr ⟨a', ha'⟩ - simp only [Nat.succ_eq_add_one, insertLiftSome, insertLift] - exact Subtype.ext ha'' + rcases Finset.mem_insert.mp a.2 with ha | ha + · exact ⟨Sum.inl (), Subtype.ext ha.symm⟩ + · obtain ⟨a', ha', ha''⟩ := Finset.mem_map.mp ha + exact ⟨Sum.inr ⟨a', ha'⟩, Subtype.ext ha''⟩ lemma insertLiftSome_bijective {c : WickContraction n} (i : Fin n.succ) (j : c.uncontracted) : Function.Bijective (insertLiftSome i j) := @@ -743,60 +445,19 @@ lemma insertLiftSome_bijective {c : WickContraction n} (i : Fin n.succ) (j : c.u set_option backward.isDefEq.respectTransparency false in lemma insertAndContractNat_injective (i : Fin n.succ) : - Function.Injective (fun c => insertAndContractNat c i none) := by - intro c1 c2 hc1c2 - rw [Subtype.ext_iff] at hc1c2 - simp [insertAndContractNat] at hc1c2 - exact Subtype.ext hc1c2 + Function.Injective (fun c => insertAndContractNat c i none) := fun _ _ hc => + Subtype.ext (by simpa [insertAndContractNat] using Subtype.ext_iff.mp hc) lemma insertAndContractNat_surjective_on_nodual (i : Fin n.succ) (c : WickContraction n.succ) (hc : c.getDual? i = none) : ∃ c', insertAndContractNat c' i none = c := by - use c.erase i - apply Subtype.ext - ext a - simp [insertAndContractNat, erase] - apply Iff.intro - · intro h - obtain ⟨a', ha', rfl⟩ := h - exact ha' - · intro h - have hi : i ∈ c.uncontracted := by simpa [uncontracted] using hc - rw [mem_uncontracted_iff_not_contracted] at hi - obtain ⟨j, hj⟩ := (@Fin.exists_succAbove_eq_iff _ i (c.fstFieldOfContract ⟨a, h⟩)).mpr - (by - by_contra hn - apply hi a h - change i ∈ (⟨a, h⟩ : c.1).1 - rw [finset_eq_fstFieldOfContract_sndFieldOfContract c ⟨a, h⟩] - subst hn - simp) - obtain ⟨k, hk⟩ := (@Fin.exists_succAbove_eq_iff _ i (c.sndFieldOfContract ⟨a, h⟩)).mpr - (by - by_contra hn - apply hi a h - change i ∈ (⟨a, h⟩ : c.1).1 - rw [finset_eq_fstFieldOfContract_sndFieldOfContract c ⟨a, h⟩] - subst hn - simp) - use {j, k} - rw [Finset.mapEmbedding_apply] - simp only [Finset.map_insert, Fin.succAboveEmb_apply, Finset.map_singleton] - rw [hj, hk] - rw [← finset_eq_fstFieldOfContract_sndFieldOfContract c ⟨a, h⟩] - simp only [and_true] - exact h + have h0 : c.getDualErase i = none := Option.not_isSome_iff_eq_none.mp (by simp [hc]) + exact ⟨c.erase i, h0 ▸ erase_insert c i⟩ lemma insertAndContractNat_bijective (i : Fin n.succ) : Function.Bijective (fun c => (⟨insertAndContractNat c i none, by simp⟩ : {c : WickContraction n.succ // c.getDual? i = none})) := by - apply And.intro - · intro a b hab - simp only [Nat.succ_eq_add_one, Subtype.mk.injEq] at hab - exact insertAndContractNat_injective i hab - · intro c - obtain ⟨c', hc'⟩ := insertAndContractNat_surjective_on_nodual i c c.2 - use c' - simp [hc'] + refine ⟨fun a b hab => insertAndContractNat_injective i (by simpa using hab), fun c => ?_⟩ + exact (insertAndContractNat_surjective_on_nodual i c c.2).imp fun _ => Subtype.ext end WickContraction diff --git a/Physlib/QFT/PerturbationTheory/WickContraction/Sign/InsertSome.lean b/Physlib/QFT/PerturbationTheory/WickContraction/Sign/InsertSome.lean index 8087002ef..7bc80c2f4 100644 --- a/Physlib/QFT/PerturbationTheory/WickContraction/Sign/InsertSome.lean +++ b/Physlib/QFT/PerturbationTheory/WickContraction/Sign/InsertSome.lean @@ -37,36 +37,20 @@ lemma stat_ofFinset_eq_one_of_gradingCompliant (φs : List 𝓕.FieldOp) (hnon : ∀ i, φsΛ.getDual? i = none → i ∉ a) (hsom : ∀ i, (h : (φsΛ.getDual? i).isSome) → i ∈ a → (φsΛ.getDual? i).get h ∈ a) : (𝓕 |>ₛ ⟨φs.get, a⟩) = 1 := by - rw [ofFinset_eq_prod] - let e2 : Fin φs.length ≃ {x // (φsΛ.getDual? x).isSome} ⊕ {x // ¬ (φsΛ.getDual? x).isSome} := by - exact (Equiv.sumCompl fun a => (φsΛ.getDual? a).isSome = true).symm - rw [← e2.symm.prod_comp] + rw [ofFinset_eq_prod, ← (Equiv.sumCompl fun a => (φsΛ.getDual? a).isSome = true).prod_comp] simp only [Fin.getElem_fin, Fintype.prod_sum_type] conv_lhs => enter [2, 2, x] - simp only [Equiv.symm_symm, Equiv.sumCompl_apply_inl, Equiv.sumCompl_apply_inr, e2] - rw [if_neg (hnon x.1 (by simpa using x.2))] - simp only [Equiv.symm_symm, Equiv.sumCompl_apply_inl, Finset.prod_const_one, mul_one, e2] - rw [← φsΛ.sigmaContractedEquiv.prod_comp] - rw [Fintype.prod_sigma] - apply Fintype.prod_eq_one _ - intro x + rw [Equiv.sumCompl_apply_inr, if_neg (hnon x.1 (by simpa using x.2))] + simp only [Equiv.sumCompl_apply_inl, Finset.prod_const_one, mul_one] + rw [← φsΛ.sigmaContractedEquiv.prod_comp, Fintype.prod_sigma] + refine Fintype.prod_eq_one _ fun x => ?_ rw [prod_finset_eq_mul_fst_snd] simp only [sigmaContractedEquiv, Equiv.coe_fn_mk, mul_ite, ite_mul, one_mul, mul_one] - split - · split - rw [hg x] - simp only [mul_self] - rename_i h1 h2 - have hsom' := hsom (φsΛ.sndFieldOfContract x) (by simp) h1 - simp only [sndFieldOfContract_getDual?, Option.get_some] at hsom' - exact False.elim (h2 hsom') - · split - rename_i h1 h2 - have hsom' := hsom (φsΛ.fstFieldOfContract x) (by simp) h2 - simp only [fstFieldOfContract_getDual?, Option.get_some] at hsom' - exact False.elim (h1 hsom') - rfl + have h1 := hsom (φsΛ.fstFieldOfContract x) (by simp) + have h2 := hsom (φsΛ.sndFieldOfContract x) (by simp) + simp only [fstFieldOfContract_getDual?, sndFieldOfContract_getDual?, Option.get_some] at h1 h2 + split <;> split <;> simp_all [hg x] lemma signFinset_insertAndContract_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (i1 i2 : Fin φs.length) @@ -85,125 +69,35 @@ lemma signFinset_insertAndContract_some (φ : 𝓕.FieldOp) (φs : List 𝓕.Fie ext k rcases insert_fin_eq_self φ i k with hk | hk · subst hk - have h1 : Fin.cast (insertIdx_length_fin φ φs i).symm i ∈ - (if i.succAbove i1 < i ∧ i < i.succAbove i2 ∧ (i1 < j) then - Insert.insert (finCongr (insertIdx_length_fin φ φs i).symm i) - (insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2)) - else - if i1 < j ∧ j < i2 ∧ ¬ i.succAbove i1 < i then - (insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2)).erase - (finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j)) - else - (insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2))) ↔ - i.succAbove i1 < i ∧ i < i.succAbove i2 ∧ (i1 < j) := by - split - simp_all only [Nat.succ_eq_add_one, finCongr_apply, Finset.mem_insert, - self_not_mem_insertAndContractLiftFinset, or_false, and_self] - rename_i h - simp only [Nat.succ_eq_add_one, not_lt, finCongr_apply, h, iff_false] - split - simp only [Finset.mem_erase, ne_eq, self_not_mem_insertAndContractLiftFinset, and_false, - not_false_eq_true] - simp - rw [h1] simp only [Nat.succ_eq_add_one, signFinset, finCongr_apply, Finset.mem_filter, Finset.mem_univ, insertAndContract_some_getDual?_self_eq, reduceCtorEq, Option.isSome_some, Option.get_some, - forall_const, false_or, true_and] - rw [Fin.lt_def, Fin.lt_def, Fin.lt_def, Fin.lt_def] - simp only [Fin.val_cast, Fin.val_fin_lt, and_congr_right_iff] - intro h1 h2 - exact Fin.succAbove_lt_succAbove_iff + forall_const, false_or, true_and, Fin.cast_lt_cast, Fin.succAbove_lt_succAbove_iff] + split + · simp_all + · rename_i h + simp only [h, false_iff] + split <;> simp · obtain ⟨k, hk⟩ := hk subst hk by_cases hkj : k = j.1 · subst hkj - conv_lhs=> simp only [Nat.succ_eq_add_one, signFinset, finCongr_apply, Finset.mem_filter, + have hj : φsΛ.getDual? ↑j = none := (φsΛ.getDual?_eq_none_iff_mem_uncontracted ↑j).mpr j.2 + simp only [Nat.succ_eq_add_one, signFinset, finCongr_apply, Finset.mem_filter, Finset.mem_univ, insertAndContract_some_getDual?_some_eq, reduceCtorEq, Option.isSome_some, - Option.get_some, forall_const, false_or, true_and, not_lt] - rw [Fin.lt_def, Fin.lt_def] - simp only [Fin.val_cast, Fin.val_fin_lt, Nat.succ_eq_add_one, finCongr_apply, not_lt] - conv_lhs => - enter [2, 2] - rw [Fin.lt_def] - simp only [Fin.val_cast, Fin.val_fin_lt] + Option.get_some, forall_const, false_or, true_and, Fin.cast_lt_cast, + Fin.succAbove_lt_succAbove_iff] split - · rename_i h - simp_all only [and_true, Finset.mem_insert] - rw [succAbove_mem_insertAndContractLiftFinset] - simp only [Fin.ext_iff, Fin.val_cast] - have h1 : ¬ (i.succAbove ↑j) = i := Fin.succAbove_ne i ↑j - simp only [Fin.val_eq_val, h1, signFinset, Finset.mem_filter, Finset.mem_univ, true_and, - false_or] - rw [Fin.succAbove_lt_succAbove_iff, Fin.succAbove_lt_succAbove_iff] - simp only [and_congr_right_iff, iff_self_and] - intro h1 h2 - apply Or.inl - have hj:= j.2 - simpa [uncontracted, -SetLike.coe_mem] using hj - · rename_i h - simp only [not_and, not_lt] at h - rw [Fin.succAbove_lt_succAbove_iff, Fin.succAbove_lt_succAbove_iff] - split - · rename_i h1 - simp only [Finset.mem_erase, ne_eq, not_true_eq_false, false_and, iff_false, not_and, - not_lt] - intro h1 h2 - omega - · rename_i h1 - rw [succAbove_mem_insertAndContractLiftFinset] - simp only [signFinset, Finset.mem_filter, Finset.mem_univ, true_and, and_congr_right_iff] - intro h1 h2 - have hj:= j.2 - simp only [uncontracted, Finset.mem_filter, Finset.mem_univ, true_and] at hj - simp only [hj, Option.isSome_none, Bool.false_eq_true, IsEmpty.forall_iff, or_self, - iff_true, gt_iff_lt] - omega - · have h1 : Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove k) ∈ - (if i.succAbove i1 < i ∧ i < i.succAbove i2 ∧ (i1 < j) then - Insert.insert (finCongr (insertIdx_length_fin φ φs i).symm i) - (insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2)) - else - if i1 < j ∧ j < i2 ∧ ¬ i.succAbove i1 < i then - (insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2)).erase - (finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j)) - else - (insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2))) ↔ - Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove k) ∈ - (insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2)) := by - split - · simp only [Nat.succ_eq_add_one, finCongr_apply, Finset.mem_insert, or_iff_right_iff_imp] - intro h - simp only [Fin.ext_iff, Fin.val_cast] at h - simp only [Fin.val_eq_val] at h - have hn : ¬ i.succAbove k = i := Fin.succAbove_ne i k - exact False.elim (hn h) - · split - simp only [Nat.succ_eq_add_one, finCongr_apply, Finset.mem_erase, ne_eq, - and_iff_right_iff_imp] - intro h - simp only [Fin.ext_iff, Fin.val_cast] - simp only [Fin.val_eq_val] - rw [Function.Injective.eq_iff] - exact hkj - exact Fin.succAbove_right_injective - · simp - rw [h1] - rw [succAbove_mem_insertAndContractLiftFinset] - simp only [Nat.succ_eq_add_one, signFinset, finCongr_apply, Finset.mem_filter, - Finset.mem_univ, true_and] - rw [Fin.lt_def, Fin.lt_def, Fin.lt_def, Fin.lt_def] - simp only [Fin.val_cast, Fin.val_fin_lt] - rw [Fin.succAbove_lt_succAbove_iff, Fin.succAbove_lt_succAbove_iff] - simp only [and_congr_right_iff] - intro h1 h2 - simp only [ne_eq, hkj, not_false_eq_true, insertAndContract_some_succAbove_getDual?_eq_option, - Nat.succ_eq_add_one, Option.map_eq_none_iff, Option.isSome_map] - conv_lhs => - rhs - enter [h] - rw [Fin.lt_def] - simp only [Fin.val_cast, Option.get_map, Function.comp_apply, Fin.val_fin_lt] - rw [Fin.succAbove_lt_succAbove_iff] + · simp_all [succAbove_mem_insertAndContractLiftFinset, Fin.cast_inj, Fin.succAbove_ne] + · split <;> simp_all [succAbove_mem_insertAndContractLiftFinset] + · simp only [Nat.succ_eq_add_one, signFinset, finCongr_apply, Finset.mem_filter, + Finset.mem_univ, true_and, ne_eq, hkj, not_false_eq_true, + insertAndContract_some_succAbove_getDual?_eq_option, Option.map_eq_none_iff, + Option.isSome_map, Option.get_map, Function.comp_apply, Fin.cast_lt_cast, + Fin.succAbove_lt_succAbove_iff] + split + · simp [Fin.cast_inj, Fin.succAbove_ne, succAbove_mem_insertAndContractLiftFinset] + · split <;> simp [Fin.cast_inj, Fin.succAbove_right_injective.eq_iff, hkj, + succAbove_mem_insertAndContractLiftFinset] /-- Given a Wick contraction `φsΛ` the sign defined in the following way, @@ -250,8 +144,8 @@ def signInsertSome (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickCo lemma sign_insert_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) : (φsΛ ↩Λ φ i (some j)).sign = (φsΛ.signInsertSome φ φs i j) * φsΛ.sign := by - rw [sign, signInsertSome, signInsertSomeProd, sign, mul_assoc, ← Finset.prod_mul_distrib] - rw [insertAndContract_some_prod_contractions] + rw [sign, signInsertSome, signInsertSomeProd, sign, mul_assoc, ← Finset.prod_mul_distrib, + insertAndContract_some_prod_contractions] congr funext a simp only [Nat.succ_eq_add_one, insertAndContract_sndFieldOfContract, @@ -259,32 +153,21 @@ lemma sign_insert_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : Wi insertAndContract_fstFieldOfContract, not_lt, ite_mul, one_mul] erw [signFinset_insertAndContract_some] split - · rename_i h - simp only [Nat.succ_eq_add_one, finCongr_apply] - rw [ofFinset_insert] - simp only [Fin.getElem_fin, Fin.val_cast, List.getElem_insertIdx_self, map_mul] - rw [stat_ofFinset_of_insertAndContractLiftFinset] - simp only [exchangeSign_symm] - simp - · rename_i h - split - · rename_i h1 + · simp only [Nat.succ_eq_add_one, finCongr_apply] + rw [ofFinset_insert _ _ _ _ (self_not_mem_insertAndContractLiftFinset φ i _), + stat_ofFinset_of_insertAndContractLiftFinset] + simp [List.getElem_insertIdx_self, exchangeSign_symm] + · split + · rename_i h h1 simp only [Nat.succ_eq_add_one, finCongr_apply, h1, true_and] - rw [if_pos] - rw [ofFinset_erase] - simp only [Fin.getElem_fin, Fin.val_cast, insertIdx_getElem_fin, map_mul] - rw [stat_ofFinset_of_insertAndContractLiftFinset] - simp only [exchangeSign_symm] + rw [if_pos, ofFinset_erase, stat_ofFinset_of_insertAndContractLiftFinset] + simp only [Fin.getElem_fin, Fin.val_cast, insertIdx_getElem_fin, map_mul, + exchangeSign_symm] · rw [succAbove_mem_insertAndContractLiftFinset] simp only [signFinset, Finset.mem_filter, Finset.mem_univ, true_and] - simp_all only [Nat.succ_eq_add_one, and_true, false_and, not_false_eq_true, not_lt, - true_and] - apply Or.inl - simpa [uncontracted, -SetLike.coe_mem] using j.2 + exact ⟨h1.1, h1.2.1, Or.inl ((φsΛ.getDual?_eq_none_iff_mem_uncontracted ↑j).mpr j.2)⟩ · simp_all - · rename_i h1 - rw [if_neg] - rw [stat_ofFinset_of_insertAndContractLiftFinset] + · rw [if_neg, stat_ofFinset_of_insertAndContractLiftFinset] simp_all lemma signInsertSomeProd_eq_one_if (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) @@ -303,22 +186,10 @@ lemma signInsertSomeProd_eq_one_if (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) congr funext a split - · rename_i h - simp only [Fin.getElem_fin, h, Nat.succ_eq_add_one, and_self, - not_true_eq_false, and_false, or_false, ↓reduceIte] - · rename_i h - split - · rename_i h1 - simp only [Fin.getElem_fin, h1, Nat.succ_eq_add_one, false_and, - not_false_eq_true, and_self, or_true, ↓reduceIte] - congr 1 - exact congrArg (⇑exchangeSign) (id (Eq.symm hφj)) - · rename_i h1 - simp only [Nat.succ_eq_add_one, not_lt, Fin.getElem_fin] - rw [if_neg] - simp_all only [Fin.getElem_fin, Nat.succ_eq_add_one, not_and, not_lt, not_le, not_or, - implies_true, and_true] - omega + · rw [if_pos (by omega)] + · split + · rw [hφj, if_pos (by omega)] + · rw [if_neg (by omega)] lemma signInsertSomeProd_eq_prod_prod (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) @@ -333,25 +204,17 @@ lemma signInsertSomeProd_eq_prod_prod (φ : 𝓕.FieldOp) (φs : List 𝓕.Field 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs[x.1]) else 1 := by - rw [signInsertSomeProd_eq_one_if] + rw [signInsertSomeProd_eq_one_if (hφj := hφj)] congr funext a rw [prod_finset_eq_mul_fst_snd] nth_rewrite 3 [if_neg] · simp only [Nat.succ_eq_add_one, not_lt, Fin.getElem_fin, - fstFieldOfContract_getDual?, Option.get_some, mul_one] - congr 1 - rw [hg a] - · simp only [Nat.succ_eq_add_one, sndFieldOfContract_getDual?, Option.get_some, not_lt, not_and, - not_or, not_le] - intro h1 + fstFieldOfContract_getDual?, Option.get_some, mul_one, hg a] + · simp only [sndFieldOfContract_getDual?, Option.get_some] have ha := fstFieldOfContract_lt_sndFieldOfContract φsΛ a - apply And.intro - · intro hi - have hx := (Fin.succAbove_lt_succAbove_iff (p := i)).mpr ha - omega - · omega - simp [hφj] + have hx := (Fin.succAbove_lt_succAbove_iff (p := i)).mpr ha + omega lemma signInsertSomeProd_eq_prod_fin (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) @@ -365,25 +228,11 @@ lemma signInsertSomeProd_eq_prod_fin (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldO then 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs[x.1]) else 1 else 1 := by - rw [signInsertSomeProd_eq_prod_prod, Finset.prod_sigma'] + rw [signInsertSomeProd_eq_prod_prod (hφj := hφj) (hg := hg), Finset.prod_sigma'] erw [← φsΛ.sigmaContractedEquiv.symm.prod_comp] - let e2 : Fin φs.length ≃ {x // (φsΛ.getDual? x).isSome} ⊕ {x // ¬ (φsΛ.getDual? x).isSome} := by - exact (Equiv.sumCompl fun a => (φsΛ.getDual? a).isSome = true).symm - rw [← e2.symm.prod_comp] - simp only [Fin.getElem_fin, Fintype.prod_sum_type] - conv_rhs => - rhs - enter [2, a] - rw [dif_neg (by simpa [e2] using a.2)] - conv_rhs => - lhs - enter [2, a] - rw [dif_pos (by simpa [e2] using a.2)] - simp only [Nat.succ_eq_add_one, not_lt, Equiv.symm_symm, Equiv.sumCompl_apply_inl, - Finset.prod_const_one, mul_one, e2] + rw [Fintype.prod_dite] + simp only [Finset.prod_const_one, mul_one] rfl - simp only [hφj, Fin.getElem_fin] - exact hg lemma signInsertSomeProd_eq_finset (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) @@ -394,23 +243,14 @@ lemma signInsertSomeProd_eq_finset (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) ∀ (h : (φsΛ.getDual? x).isSome), x < j ∧ (i.succAbove x < i ∧ i < i.succAbove ((φsΛ.getDual? x).get h) ∨ j < ((φsΛ.getDual? x).get h) ∧ ¬ i.succAbove x < i)))⟩) := by - rw [signInsertSomeProd_eq_prod_fin, ofFinset_eq_prod] - rw [map_prod] + rw [signInsertSomeProd_eq_prod_fin (hφj := hφj) (hg := hg), ofFinset_eq_prod, map_prod] congr funext x - split - · rename_i h - simp only [Nat.succ_eq_add_one, not_lt, Finset.mem_filter, Finset.mem_univ, + split <;> rename_i h + · simp only [Nat.succ_eq_add_one, not_lt, Finset.mem_filter, Finset.mem_univ, h, forall_true_left, true_and, Fin.getElem_fin] - split - · rename_i h1 - simp - · rename_i h1 - simp - · rename_i h - simp [h] - simp only [hφj, Fin.getElem_fin] - exact hg + split <;> simp + · simp [h] lemma signInsertSomeCoef_if (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) (hφj : (𝓕 |>ₛ φ) = (𝓕 |>ₛ φs[j.1])) : @@ -424,12 +264,9 @@ lemma signInsertSomeCoef_if (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ signFinset (φsΛ ↩Λ φ i (some j)) (finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j)) (finCongr (insertIdx_length_fin φ φs i).symm i)⟩) := by - simp only [signInsertSomeCoef, Nat.succ_eq_add_one, - insertAndContract_sndFieldOfContract_some_incl, finCongr_apply, Fin.getElem_fin, + simp only [signInsertSomeCoef, insertAndContract_sndFieldOfContract_some_incl, insertAndContract_fstFieldOfContract_some_incl] - split - · simp [hφj] - · simp [hφj] + split <;> simp [hφj] lemma stat_signFinset_insert_some_self_fst (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) @@ -440,72 +277,28 @@ lemma stat_signFinset_insert_some_self_fst 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun x => i < i.succAbove x ∧ x < j ∧ ((φsΛ.getDual? x = none) ∨ ∀ (h : (φsΛ.getDual? x).isSome), i < i.succAbove ((φsΛ.getDual? x).get h))))⟩ := by - rw [get_eq_insertIdx_succAbove φ _ i, ofFinset_finset_map] - swap - refine - (Equiv.comp_injective i.succAbove (finCongr (Eq.symm (insertIdx_length_fin φ φs i)))).mpr ?hi.a - exact Fin.succAbove_right_injective + rw [get_eq_insertIdx_succAbove φ _ i, ofFinset_finset_map _ _ + ((Equiv.comp_injective _ _).mpr Fin.succAbove_right_injective)] congr ext x simp only [Nat.succ_eq_add_one, signFinset, finCongr_apply, Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_map, Function.Embedding.coeFn_mk, Function.comp_apply] rcases insert_fin_eq_self φ i x with hx | hx · subst hx - simp only [Nat.succ_eq_add_one, lt_self_iff_false, insertAndContract_some_getDual?_self_eq, - reduceCtorEq, Option.isSome_some, Option.get_some, forall_const, false_or, and_self, - false_and, false_iff, not_exists, not_and, and_imp] - intro x hi hx h - simp only [Fin.ext_iff, Fin.val_cast] - simp only [Fin.val_eq_val] - exact Fin.succAbove_ne i x + simp [Fin.cast_inj, Fin.succAbove_ne] · obtain ⟨x, hx⟩ := hx subst hx by_cases h : x = j.1 · subst h simp only [Nat.succ_eq_add_one, lt_self_iff_false, insertAndContract_some_getDual?_some_eq, reduceCtorEq, Option.isSome_some, Option.get_some, imp_false, not_true_eq_false, or_self, - and_self, and_false, false_iff, not_exists, not_and, and_imp] - intro x hi hx h0 - simp only [Fin.ext_iff, Fin.val_cast] - simp only [Fin.val_eq_val] - rw [Function.Injective.eq_iff] + and_self, and_false, false_iff, not_exists, not_and, and_imp, Fin.cast_inj, + Fin.succAbove_right_injective.eq_iff] omega - exact Fin.succAbove_right_injective · simp only [Nat.succ_eq_add_one, ne_eq, h, not_false_eq_true, insertAndContract_some_succAbove_getDual?_eq_option, Option.map_eq_none_iff, - Option.isSome_map] - rw [Fin.lt_def, Fin.lt_def] - simp only [Fin.val_cast, Fin.val_fin_lt] - apply Iff.intro - · intro h - use x - simp only [h, true_and, and_true] - simp only [Option.get_map, Function.comp_apply] at h - apply And.intro (Fin.succAbove_lt_succAbove_iff.mp h.2.1) - have h2 := h.2.2 - rcases h2 with h2 | h2 - · simp [h2] - · apply Or.inr - intro h - have h2 := h2 h - simpa using h2 - · intro h - obtain ⟨y, hy1, hy2⟩ := h - simp only [Fin.ext_iff, Fin.val_cast] at hy2 - simp only [Fin.val_eq_val] at hy2 - rw [Function.Injective.eq_iff (Fin.succAbove_right_injective)] at hy2 - subst hy2 - simp only [hy1, true_and] - apply And.intro - · rw [@Fin.succAbove_lt_succAbove_iff] - omega - · have hy2 := hy1.2.2 - rcases hy2 with hy2 | hy2 - · simp [hy2] - · apply Or.inr - intro h - have hy2 := hy2 h - simpa [Option.get_map] using hy2 + Option.isSome_map, Option.get_map, Function.comp_apply, Fin.cast_lt_cast, Fin.cast_inj, + Fin.succAbove_right_injective.eq_iff, exists_eq_right, Fin.succAbove_lt_succAbove_iff] lemma stat_signFinset_insert_some_self_snd (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) : @@ -516,76 +309,28 @@ lemma stat_signFinset_insert_some_self_snd (φ : 𝓕.FieldOp) (φs : List 𝓕. 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun x => j < x ∧ i.succAbove x < i ∧ ((φsΛ.getDual? x = none) ∨ ∀ (h : (φsΛ.getDual? x).isSome), j < ((φsΛ.getDual? x).get h))))⟩ := by - rw [get_eq_insertIdx_succAbove φ _ i, ofFinset_finset_map] - swap - refine - (Equiv.comp_injective i.succAbove (finCongr (Eq.symm (insertIdx_length_fin φ φs i)))).mpr ?hi.a - exact Fin.succAbove_right_injective + rw [get_eq_insertIdx_succAbove φ _ i, ofFinset_finset_map _ _ + ((Equiv.comp_injective _ _).mpr Fin.succAbove_right_injective)] congr ext x simp only [Nat.succ_eq_add_one, signFinset, finCongr_apply, Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_map, Function.Embedding.coeFn_mk, Function.comp_apply] rcases insert_fin_eq_self φ i x with hx | hx · subst hx - simp only [Nat.succ_eq_add_one, lt_self_iff_false, insertAndContract_some_getDual?_self_eq, - reduceCtorEq, Option.isSome_some, Option.get_some, imp_false, not_true_eq_false, or_self, - and_self, and_false, false_iff, not_exists, not_and, and_imp] - intro x hi hx h - simp only [Fin.ext_iff, Fin.val_cast] - simp only [Fin.val_eq_val] - exact Fin.succAbove_ne i x + simp [Fin.cast_inj, Fin.succAbove_ne] · obtain ⟨x, hx⟩ := hx subst hx by_cases h : x = j.1 · subst h simp only [Nat.succ_eq_add_one, lt_self_iff_false, insertAndContract_some_getDual?_some_eq, reduceCtorEq, Option.isSome_some, Option.get_some, forall_const, false_or, and_self, - false_and, false_iff, not_exists, not_and, and_imp] - intro x hi hx h0 - simp only [Fin.ext_iff, Fin.val_cast] - simp only [Fin.val_eq_val] - rw [Function.Injective.eq_iff] + false_and, false_iff, not_exists, not_and, and_imp, Fin.cast_inj, + Fin.succAbove_right_injective.eq_iff] omega - exact Fin.succAbove_right_injective · simp only [Nat.succ_eq_add_one, ne_eq, h, not_false_eq_true, insertAndContract_some_succAbove_getDual?_eq_option, Option.map_eq_none_iff, - Option.isSome_map] - rw [Fin.lt_def, Fin.lt_def] - simp only [Fin.val_cast, Fin.val_fin_lt] - apply Iff.intro - · intro h - use x - simp only [h, true_and, and_true] - simp only [Option.get_map, Function.comp_apply] at h - apply And.intro (Fin.succAbove_lt_succAbove_iff.mp h.1) - have h2 := h.2.2 - rcases h2 with h2 | h2 - · simp [h2] - · apply Or.inr - intro h - have h2 := h2 h - rw [Fin.lt_def] at h2 - simp only [Fin.val_cast, Fin.val_fin_lt] at h2 - exact Fin.succAbove_lt_succAbove_iff.mp h2 - · intro h - obtain ⟨y, hy1, hy2⟩ := h - simp only [Fin.ext_iff, Fin.val_cast] at hy2 - simp only [Fin.val_eq_val] at hy2 - rw [Function.Injective.eq_iff (Fin.succAbove_right_injective)] at hy2 - subst hy2 - simp only [hy1, true_and] - apply And.intro - · rw [@Fin.succAbove_lt_succAbove_iff] - omega - · have hy2 := hy1.2.2 - rcases hy2 with hy2 | hy2 - · simp [hy2] - · apply Or.inr - intro h - have hy2 := hy2 h - simp only [Fin.lt_def, Fin.val_cast, gt_iff_lt] - simp only [Option.get_map, Function.comp_apply, Fin.val_cast, Fin.val_fin_lt] - exact Fin.succAbove_lt_succAbove_iff.mpr hy2 + Option.isSome_map, Option.get_map, Function.comp_apply, Fin.cast_lt_cast, Fin.cast_inj, + Fin.succAbove_right_injective.eq_iff, exists_eq_right, Fin.succAbove_lt_succAbove_iff] lemma signInsertSomeCoef_eq_finset (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) @@ -644,91 +389,32 @@ lemma signInsertSome_mul_filter_contracted_of_lt (φ : 𝓕.FieldOp) (φs : List rw [Finset.disjoint_filter] intro j _ h simp only [Nat.succ_eq_add_one, not_lt, not_and, not_forall, not_or, not_le] - intro h1 - use h1 - omega + exact fun h1 => ⟨h1, by omega⟩ rw [ofFinset_union, ← mul_eq_one_iff, ofFinset_union] simp only [Nat.succ_eq_add_one, not_lt] apply stat_ofFinset_eq_one_of_gradingCompliant _ _ _ hg.1 · /- The `c.getDual? i = none` case for `stat_ofFinset_eq_one_of_gradingCompliant`. -/ intro j hn + have h1 := Fin.succAbove_le_succAbove_iff (p := i) (i := j) (j := k.1) + have h2 := Fin.ne_succAbove i j simp only [uncontracted, Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_univ, hn, Option.isSome_none, Bool.false_eq_true, IsEmpty.forall_iff, or_self, and_true, or_false, true_and, and_self, Finset.mem_inter, not_and, not_lt, Classical.not_imp, not_le, and_imp] - intro h - rcases h with h | h - · simp only [h, or_true, isEmpty_Prop, not_le, IsEmpty.forall_iff, and_self] - · simp only [h, true_and] - refine And.intro ?_ (And.intro ?_ h.2) - · by_contra hkj - simp only [not_lt] at hkj - have h2 := h.2 hkj - apply Fin.ne_succAbove i j - have hij : i.succAbove j ≤ i.succAbove k.1 := Fin.succAbove_le_succAbove_iff.mpr hkj - omega - · have h1' := h.1 - rcases h1' with h1' | h1' - · have hl := h.2 h1' - have hij : i.succAbove j ≤ i.succAbove k.1 := Fin.succAbove_le_succAbove_iff.mpr h1' - by_contra hn - apply Fin.ne_succAbove i j - omega - · exact h1' + omega · /- The `(c.getDual? i).isSome` case for `stat_ofFinset_eq_one_of_gradingCompliant`. -/ intro j hj have hn : ¬ φsΛ.getDual? j = none := Option.isSome_iff_ne_none.mp hj + have hkd := (φsΛ.getDual?_eq_none_iff_mem_uncontracted _).mpr k.2 + have hkneqj : ↑k ≠ j := fun h => by simp [h ▸ hkd] at hj + have hkneqdual : k.1 ≠ (φsΛ.getDual? j).get hj := fun h => by simp [h] at hkd + have h2' := Fin.ne_succAbove i ((φsΛ.getDual? j).get hj) + have m1 := Fin.succAbove_lt_succAbove_iff (p := i) (i := j) (j := k.1) + have m2 := Fin.succAbove_lt_succAbove_iff (p := i) (i := (φsΛ.getDual? j).get hj) (j := k.1) simp only [uncontracted, Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_univ, hn, hj, forall_true_left, false_or, true_and, and_false, false_and, Finset.mem_inter, not_false_eq_true, and_true, not_and, not_lt, getDual?_getDual?_get_get, reduceCtorEq, Option.isSome_some, Option.get_some, forall_const, and_imp] - intro h1 h2 - have hijsucc' : i.succAbove ((φsΛ.getDual? j).get hj) ≠ i := Fin.succAbove_ne i _ - have hkneqj : ↑k ≠ j := by - by_contra hkj - have hk := k.prop - simp only [uncontracted, Finset.mem_filter, Finset.mem_univ, true_and] at hk - simp_all - have hkneqgetdual : k.1 ≠ (φsΛ.getDual? j).get hj := by - by_contra hkj - have hk := k.prop - simp only [uncontracted, Finset.mem_filter, Finset.mem_univ, true_and] at hk - simp_all - by_cases hik : ↑k < j - · have hn : ¬ j < ↑k := by omega - simp only [hik, true_and, hn, false_and, or_false, and_imp, and_true] at h1 h2 ⊢ - have hir : i.succAbove j < i := by - rcases h1 with h1 | h1 - · simp [h1] - · simp [h1] - simp only [hir, true_and, or_true, forall_const] at h1 h2 - have hnkdual : ¬ ↑k < (φsΛ.getDual? j).get hj := by - by_contra hn - have h2 := h2 hn - apply Fin.ne_succAbove i j - omega - simp only [hnkdual, IsEmpty.forall_iff, false_and, false_or, and_imp] at h2 ⊢ - have hnkdual : (φsΛ.getDual? j).get hj < ↑k := by omega - have hi : i.succAbove ((φsΛ.getDual? j).get hj) < i.succAbove k := by - rw [@Fin.succAbove_lt_succAbove_iff] - omega - omega - · have ht : j < ↑k := by omega - have ht' : i.succAbove j < i.succAbove k := by - rw [@Fin.succAbove_lt_succAbove_iff] - omega - simp only [hik, false_and, ht, true_and, false_or, and_false, or_false, and_imp] at h1 h2 ⊢ - by_cases hik : i.succAbove j < i - · simp_all only [Fin.getElem_fin, ne_eq, not_lt, true_and, or_true] - have hn : ¬ i ≤ i.succAbove j := by omega - simp_all only [and_false, or_false, imp_false, not_lt, Nat.succ_eq_add_one, not_le] - apply And.intro - · apply Or.inr - omega - · intro h1 h2 h3 - omega - · simp_all only [Fin.getElem_fin, ne_eq, not_lt, false_and, false_or, or_false, and_self, - or_true, imp_self] - omega + omega /-- The following two signs are equal for `i < i.succAbove k`. @@ -776,84 +462,27 @@ lemma signInsertSome_mul_filter_contracted_of_not_lt (φ : 𝓕.FieldOp) (φs : · /- The `c.getDual? i = none` case for `stat_ofFinset_eq_one_of_gradingCompliant`. -/ intro j hj have hijsucc : i.succAbove j ≠ i := Fin.succAbove_ne i j + have h1 := Fin.succAbove_lt_succAbove_iff (p := i) (i := j) (j := k.1) simp only [uncontracted, Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_univ, hj, Option.isSome_none, Bool.false_eq_true, IsEmpty.forall_iff, or_self, and_true, true_and, and_false, or_false, Finset.mem_inter, not_false_eq_true, and_self, not_and, not_lt, Classical.not_imp, not_le, and_imp] - intro h - have hij : i < i.succAbove j := by - rcases h with h | h - · exact h.1 - · rcases h.1 with h1 | h1 - · omega - · have hik : i.succAbove k.1 ≤ i.succAbove j := by - rw [Fin.succAbove_le_succAbove_iff] - omega - omega - simp only [hij, true_and] at h ⊢ omega · /- The `(c.getDual? i).isSome` case for `stat_ofFinset_eq_one_of_gradingCompliant`. -/ intro j hj have hn : ¬ φsΛ.getDual? j = none := Option.isSome_iff_ne_none.mp hj + have hkd := (φsΛ.getDual?_eq_none_iff_mem_uncontracted _).mpr k.2 + have hkneqj : ↑k ≠ j := fun h => by simp [h ▸ hkd] at hj have hijSuc : i.succAbove j ≠ i := Fin.succAbove_ne i j - have hkneqj : ↑k ≠ j := by - by_contra hkj - have hk := k.prop - simp only [uncontracted, Finset.mem_filter, Finset.mem_univ, true_and] at hk - simp_all - have hkneqgetdual : k.1 ≠ (φsΛ.getDual? j).get hj := by - by_contra hkj - have hk := k.prop - simp only [uncontracted, Finset.mem_filter, Finset.mem_univ, true_and] at hk - simp_all + have hkneqdual : k.1 ≠ (φsΛ.getDual? j).get hj := fun h => by simp [h] at hkd + have h2' := Fin.ne_succAbove i ((φsΛ.getDual? j).get hj) + have m1 := Fin.succAbove_lt_succAbove_iff (p := i) (i := j) (j := k.1) + have m2 := Fin.succAbove_lt_succAbove_iff (p := i) (i := (φsΛ.getDual? j).get hj) (j := k.1) simp only [uncontracted, Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_univ, hn, hj, forall_true_left, false_or, true_and, Finset.mem_inter, not_and, not_or, not_lt, not_le, and_imp, and_false, false_and, not_false_eq_true, and_true, getDual?_getDual?_get_get, reduceCtorEq, Option.isSome_some, Option.get_some, forall_const] - by_cases hik : ↑k < j - · have hikn : ¬ j < k.1 := by omega - have hksucc : i.succAbove k.1 < i.succAbove j := by - rw [Fin.succAbove_lt_succAbove_iff] - omega - have hkn : i < i.succAbove j := by omega - have hl : ¬ i.succAbove j < i := by omega - simp only [hkn, hikn, false_and, and_false, hl, false_or, or_self, IsEmpty.forall_iff, - imp_false, not_lt, true_and, implies_true, and_true, forall_const, hik, - imp_forall_iff_forall] - · have hikn : j < k.1 := by omega - have hksucc : i.succAbove j < i.succAbove k.1 := Fin.succAbove_lt_succAbove_iff.mpr hikn - simp only [hikn, true_and, forall_const, hik, false_and, or_false, IsEmpty.forall_iff, - and_true] - by_cases hij: i < i.succAbove j - · simp only [hij, true_and, forall_const, and_true, imp_forall_iff_forall] - have hijn : ¬ i.succAbove j < i := by omega - simp only [hijn, false_and, false_or, IsEmpty.forall_iff, imp_false, not_lt, true_and, - or_false, and_imp] - have hijle : i ≤ i.succAbove j := by omega - simp only [hijle, and_true, implies_true, forall_const] - intro h1 h2 - apply And.intro - · rcases h1 with h1 | h1 - · apply Or.inl - omega - · apply Or.inl - have hi : i.succAbove k.1 < i.succAbove ((φsΛ.getDual? j).get hj) := - Fin.succAbove_lt_succAbove_iff.mpr h1 - apply And.intro - · apply Or.inr - apply And.intro - · omega - · omega - · omega - · intro h3 h4 - omega - · simp only [hij, false_and, false_or, IsEmpty.forall_iff, and_true, forall_const, and_false, - or_self, implies_true] - have hijn : i.succAbove j < i := by omega - have hijn' : ¬ i ≤ i.succAbove j := by omega - simp only [hijn, true_and, hijn', and_false, or_false, or_true, imp_false, not_lt, - forall_const] - exact fun h => lt_of_le_of_ne h (Fin.succAbove_ne i ((φsΛ.getDual? j).get hj)) + omega /-- For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of @@ -873,12 +502,9 @@ lemma sign_insert_some_of_lt (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, φsΛ.uncontracted.filter (fun x => x ≤ ↑k)⟩) * 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, Finset.univ.filter (fun x => i.succAbove x < i)⟩) * φsΛ.sign := by - rw [sign_insert_some, - ← signInsertSome_mul_filter_contracted_of_lt φ φs φsΛ i k hk hg] - rw [← mul_assoc] + rw [sign_insert_some, ← signInsertSome_mul_filter_contracted_of_lt φ φs φsΛ i k hk hg] congr 1 - rw [mul_comm, ← mul_assoc] - simp + rw [mul_comm, mul_assoc, exchangeSign_mul_self, mul_one] /-- For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of @@ -898,12 +524,9 @@ lemma sign_insert_some_of_not_lt (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, φsΛ.uncontracted.filter (fun x => x < ↑k)⟩) * 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, Finset.univ.filter (fun x => i.succAbove x < i)⟩) * φsΛ.sign := by - rw [sign_insert_some, - ← signInsertSome_mul_filter_contracted_of_not_lt φ φs φsΛ i k hk hg] - rw [← mul_assoc] + rw [sign_insert_some, ← signInsertSome_mul_filter_contracted_of_not_lt φ φs φsΛ i k hk hg] congr 1 - rw [mul_comm, ← mul_assoc] - simp + rw [mul_comm, mul_assoc, exchangeSign_mul_self, mul_one] /-- For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of @@ -919,9 +542,6 @@ lemma sign_insert_some_zero (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (hn : GradingCompliant φs φsΛ ∧ (𝓕|>ₛφ) = 𝓕|>ₛφs[k.1]) : (φsΛ ↩Λ φ 0 k).sign = 𝓢(𝓕|>ₛφ, 𝓕 |>ₛ ⟨φs.get, (φsΛ.uncontracted.filter (fun x => x < ↑k))⟩) * φsΛ.sign := by - rw [sign_insert_some_of_not_lt] - · simp - · simp - · exact hn + simpa using sign_insert_some_of_not_lt φ φs φsΛ 0 k (by simp) hn end WickContraction From 442de4c7bb41773673fb35269a2e9278f9cb34f1 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Fri, 3 Jul 2026 21:50:39 -0700 Subject: [PATCH 3/3] refactor: golf kinetic-term and spectral-theory proofs Golf proof bodies in Electromagnetism/Dynamics/KineticTerm and QuantumMechanics SpectralTheory/Basic. Statements unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3 --- .../Dynamics/KineticTerm.lean | 535 +++++------------- .../Operators/SpectralTheory/Basic.lean | 55 +- 2 files changed, 150 insertions(+), 440 deletions(-) diff --git a/Physlib/Electromagnetism/Dynamics/KineticTerm.lean b/Physlib/Electromagnetism/Dynamics/KineticTerm.lean index ab5d6c2ee..f902d4700 100644 --- a/Physlib/Electromagnetism/Dynamics/KineticTerm.lean +++ b/Physlib/Electromagnetism/Dynamics/KineticTerm.lean @@ -105,8 +105,7 @@ lemma kineticTerm_equivariant {d} {𝓕 : FreeSpace} (A : ElectromagneticPotenti rw [kineticTerm, kineticTerm] conv_lhs => enter [2] - rw [toFieldStrength_equivariant A Λ hf, Tensorial.toTensor_smul] - rw [← actionT_coMetric Λ] + rw [toFieldStrength_equivariant A Λ hf, Tensorial.toTensor_smul, ← actionT_coMetric Λ] simp only [prodT_equivariant, contrT_equivariant, toField_equivariant] /-! @@ -179,112 +178,46 @@ lemma kineticTerm_eq_sum_fieldStrengthMatrix_sq {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (x : SpaceTime d) : A.kineticTerm 𝓕 x = - 1/(4 * 𝓕.μ₀) * ∑ μ, ∑ ν, η μ μ * η ν ν * ‖A.fieldStrengthMatrix x (μ, ν)‖ ^ 2 := by rw [kineticTerm_eq_sum_fieldStrengthMatrix] - congr - funext μ - congr - funext ν - rw [Finset.sum_eq_single μ] - · rw [Finset.sum_eq_single ν] - · simp - ring - · intro b _ hb - nth_rewrite 2 [minkowskiMatrix.off_diag_zero] - simp only [mul_zero, zero_mul] - exact id (Ne.symm hb) - · simp - · intro b _ hb - rw [Finset.sum_eq_zero] - intro ν' _ - rw [minkowskiMatrix.off_diag_zero] - simp only [zero_mul] - exact id (Ne.symm hb) - · simp + congr 1 + refine Finset.sum_congr rfl fun μ _ => Finset.sum_congr rfl fun ν _ => ?_ + rw [Finset.sum_eq_single μ (fun b _ hb => by simp [minkowskiMatrix.off_diag_zero hb.symm]) + (by simp), + Finset.sum_eq_single ν (fun b _ hb => by simp [minkowskiMatrix.off_diag_zero hb.symm]) + (by simp)] + simp [← pow_two, mul_assoc] lemma kineticTerm_eq_sum_potential {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (x : SpaceTime d) : A.kineticTerm 𝓕 x = - 1 / (2 * 𝓕.μ₀) * ∑ μ, ∑ ν, (η μ μ * η ν ν * (∂_ μ A x ν) ^ 2 - ∂_ μ A x ν * ∂_ ν A x μ) := by calc _ - _ = - 1/(4 * 𝓕.μ₀) * ∑ μ, ∑ ν, ∑ μ', ∑ ν', η μ μ' * η ν ν' * - (η μ μ * ∂_ μ A x ν - η ν ν * ∂_ ν A x μ) - * (η μ' μ' * ∂_ μ' A x ν' - η ν' ν' * ∂_ ν' A x μ') := by - rw [kineticTerm_eq_sum] - congr 1 - apply Finset.sum_congr rfl (fun μ _ => ?_) - apply Finset.sum_congr rfl (fun ν _ => ?_) - apply Finset.sum_congr rfl (fun μ' _ => ?_) - apply Finset.sum_congr rfl (fun ν' _ => ?_) - rw [toFieldStrength_basis_repr_apply_eq_single, toFieldStrength_basis_repr_apply_eq_single] - _ = - 1/(4 * 𝓕.μ₀) * ∑ μ, ∑ ν, ∑ μ', η μ μ' * η ν ν * - (η μ μ * ∂_ μ A x ν - η ν ν * ∂_ ν A x μ) - * (η μ' μ' * ∂_ μ' A x ν - η ν ν * ∂_ ν A x μ') := by - congr 1 - apply Finset.sum_congr rfl (fun μ _ => ?_) - apply Finset.sum_congr rfl (fun ν _ => ?_) - apply Finset.sum_congr rfl (fun μ' _ => ?_) - rw [Finset.sum_eq_single ν] - · intro b _ hb - nth_rewrite 2 [minkowskiMatrix.off_diag_zero] - simp only [mul_zero, zero_mul] - exact id (Ne.symm hb) - · simp _ = - 1/(4 * 𝓕.μ₀) * ∑ μ, ∑ ν, η μ μ * η ν ν * (η μ μ * ∂_ μ A x ν - η ν ν * ∂_ ν A x μ) * (η μ μ * ∂_ μ A x ν - η ν ν * ∂_ ν A x μ) := by + rw [kineticTerm_eq_sum] congr 1 - apply Finset.sum_congr rfl (fun μ _ => ?_) - apply Finset.sum_congr rfl (fun ν _ => ?_) - rw [Finset.sum_eq_single μ] - · intro b _ hb - rw [minkowskiMatrix.off_diag_zero] - simp only [zero_mul] - exact id (Ne.symm hb) - · simp - _ = - 1/(4 * 𝓕.μ₀) * ∑ μ, ∑ ν, - ((η μ μ) ^ 2 * η ν ν * ∂_ μ A x ν - (η ν ν) ^ 2 * η μ μ * ∂_ ν A x μ) - * (η μ μ * ∂_ μ A x ν - η ν ν * ∂_ ν A x μ) := by - congr 1 - apply Finset.sum_congr rfl (fun μ _ => ?_) - apply Finset.sum_congr rfl (fun ν _ => ?_) - ring - _ = - 1/(4 * 𝓕.μ₀) * ∑ μ, ∑ ν, - (η ν ν * ∂_ μ A x ν - η μ μ * ∂_ ν A x μ) - * (η μ μ * ∂_ μ A x ν - η ν ν * ∂_ ν A x μ) := by simp - _ = - 1/(4 * 𝓕.μ₀) * ∑ μ, ∑ ν, - ((η μ μ * η ν ν * (∂_ μ A x ν) ^ 2 - (η ν ν) ^ 2 * ∂_ μ A x ν * ∂_ ν A x μ) + (- - (η μ μ) ^ 2 * ∂_ ν A x μ * ∂_ μ A x ν + η μ μ * η ν ν * (∂_ ν A x μ)^2)) := by - congr 1 - apply Finset.sum_congr rfl (fun μ _ => ?_) - apply Finset.sum_congr rfl (fun ν _ => ?_) - ring + refine Finset.sum_congr rfl fun μ _ => Finset.sum_congr rfl fun ν _ => ?_ + rw [Finset.sum_eq_single μ (fun b _ hb => by simp [minkowskiMatrix.off_diag_zero hb.symm]) + (by simp), + Finset.sum_eq_single ν (fun b _ hb => by simp [minkowskiMatrix.off_diag_zero hb.symm]) + (by simp), + toFieldStrength_basis_repr_apply_eq_single] _ = - 1/(4 * 𝓕.μ₀) * ∑ μ, ∑ ν, ((η μ μ * η ν ν * (∂_ μ A x ν) ^ 2 - ∂_ μ A x ν * ∂_ ν A x μ) + - (- ∂_ ν A x μ * ∂_ μ A x ν + η μ μ * η ν ν * (∂_ ν A x μ)^2)) := by simp - _ = - 1 / (4 * 𝓕.μ₀) * ∑ μ, ∑ ν, - ((η μ μ * η ν ν * (∂_ μ A x ν) ^ 2 - ∂_ μ A x ν * ∂_ ν A x μ) + - (- ∂_ μ A x ν * ∂_ ν A x μ + η ν ν * η μ μ * (∂_ μ A x ν)^2)) := by + (η ν ν * η μ μ * (∂_ ν A x μ) ^ 2 - ∂_ ν A x μ * ∂_ μ A x ν)) := by congr 1 - conv_lhs => - enter [2, μ]; - rw [Finset.sum_add_distrib] - rw [Finset.sum_add_distrib] - conv_lhs => enter [2]; rw [Finset.sum_comm] - rw [← Finset.sum_add_distrib] - conv_lhs => - enter [2, μ]; - rw [← Finset.sum_add_distrib] - _ = - 1 / (4 * 𝓕.μ₀) * ∑ μ, ∑ ν, - (2 * (η μ μ * η ν ν * (∂_ μ A x ν) ^ 2 - ∂_ μ A x ν * ∂_ ν A x μ)) := by - congr 1 - apply Finset.sum_congr rfl (fun μ _ => ?_) - apply Finset.sum_congr rfl (fun ν _ => ?_) - ring + refine Finset.sum_congr rfl fun μ _ => Finset.sum_congr rfl fun ν _ => ?_ + linear_combination (η μ μ * η ν ν * ∂_ μ A x ν ^ 2 - + 2 * η ν ν * η ν ν * ∂_ μ A x ν * ∂_ ν A x μ) * + minkowskiMatrix.η_apply_mul_η_apply_diag μ + + (η μ μ * η ν ν * ∂_ ν A x μ ^ 2 - 2 * ∂_ μ A x ν * ∂_ ν A x μ) * + minkowskiMatrix.η_apply_mul_η_apply_diag ν _ = - 1 / (2 * 𝓕.μ₀) * ∑ μ, ∑ ν, (η μ μ * η ν ν * (∂_ μ A x ν) ^ 2 - ∂_ μ A x ν * ∂_ ν A x μ) := by + simp only [Finset.sum_add_distrib] conv_lhs => - enter [2, 2, μ] - rw [← Finset.mul_sum] - rw [← Finset.mul_sum] + enter [2, 2] + rw [Finset.sum_comm] ring /-! @@ -304,11 +237,9 @@ lemma kineticTerm_eq_electric_magnetic {𝓕 : FreeSpace} (A : ElectromagneticPo enter [2, 2, μ, 2, ν, 2, μ', 2, ν'] rw [fieldStrengthMatrix_eq_electric_magnetic A t x hA, fieldStrengthMatrix_eq_electric_magnetic A t x hA] - simp [Fintype.sum_sum_type, Fin.sum_univ_three] - rw [EuclideanSpace.norm_sq_eq, EuclideanSpace.norm_sq_eq] - simp [Fin.sum_univ_three] + simp [Fintype.sum_sum_type, Fin.sum_univ_three, EuclideanSpace.norm_sq_eq] field_simp - simp only [Fin.isValue, FreeSpace.c_sq, one_div, mul_inv_rev] + rw [FreeSpace.c_sq] field_simp ring @@ -317,10 +248,7 @@ lemma kineticTerm_eq_electric_magnetic' {𝓕 : FreeSpace} {A : ElectromagneticP A.kineticTerm 𝓕 x = 1/2 * (𝓕.ε₀ * ‖A.electricField 𝓕.c (x.time 𝓕.c) x.space‖ ^ 2 - (1 / 𝓕.μ₀) * ‖A.magneticField 𝓕.c (x.time 𝓕.c) x.space‖ ^ 2) := by - rw [← kineticTerm_eq_electric_magnetic _ _ _ hA] - congr - apply toTimeAndSpace.injective - simp + rw [← kineticTerm_eq_electric_magnetic _ _ _ hA, toTimeAndSpace_symm_apply_time_space] /-! @@ -368,9 +296,8 @@ lemma kineticTerm_eq_electricMatrix_magneticFieldMatrix {𝓕 : FreeSpace} A.kineticTerm 𝓕 x = 1/2 * (𝓕.ε₀ * ‖A.electricField 𝓕.c (x.time 𝓕.c) x.space‖ ^ 2 - (1 / (2 * 𝓕.μ₀)) * ∑ i, ∑ j, ‖A.magneticFieldMatrix 𝓕.c (x.time 𝓕.c) x.space (i, j)‖ ^ 2) := by - rw [← kineticTerm_eq_electricMatrix_magneticFieldMatrix_time_space A (x.time 𝓕.c)] - simp only [toTimeAndSpace_symm_apply_time_space] - exact hA + rw [← kineticTerm_eq_electricMatrix_magneticFieldMatrix_time_space A (x.time 𝓕.c) x.space hA, + toTimeAndSpace_symm_apply_time_space] /-! @@ -381,27 +308,13 @@ lemma kineticTerm_eq_electricMatrix_magneticFieldMatrix {𝓕 : FreeSpace} lemma kineticTerm_const {d} {𝓕 : FreeSpace} (A₀ : Lorentz.Vector d) : kineticTerm 𝓕 ⟨fun _ : SpaceTime d => A₀⟩ = 0 := by funext x - rw [kineticTerm_eq_sum_potential] - conv_lhs => - enter [2, 2, μ, 2, ν] - repeat rw [SpaceTime.deriv_eq] - simp - simp + simp [kineticTerm_eq_sum_potential, SpaceTime.deriv_eq] lemma kineticTerm_add_const {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (A₀ : Lorentz.Vector d) : kineticTerm 𝓕 ⟨fun x => A x + A₀⟩ = kineticTerm 𝓕 A := by funext x - rw [kineticTerm_eq_sum_potential, kineticTerm_eq_sum_potential] - congr - funext μ - congr - funext ν - congr - all_goals - · rw [SpaceTime.deriv_eq] - simp - rfl + simp [kineticTerm_eq_sum_potential, SpaceTime.deriv_eq] /-! @@ -412,25 +325,9 @@ lemma kineticTerm_add_const {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential lemma kineticTerm_contDiff {d} {n : WithTop ℕ∞} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (hA : ContDiff ℝ (n + 1) A) : ContDiff ℝ n (A.kineticTerm 𝓕) := by - change ContDiff ℝ n (fun x => A.kineticTerm 𝓕 x) - conv => - enter [3, x] - rw [kineticTerm_eq_sum_fieldStrengthMatrix] - apply ContDiff.mul - · fun_prop - apply ContDiff.sum - intro μ _ - apply ContDiff.sum - intro ν _ - apply ContDiff.sum - intro μ' _ - apply ContDiff.sum - intro ν' _ - apply ContDiff.mul - · apply ContDiff.mul - · fun_prop - exact fieldStrengthMatrix_contDiff hA - exact fieldStrengthMatrix_contDiff hA + rw [funext fun x => kineticTerm_eq_sum_fieldStrengthMatrix (𝓕 := 𝓕) A x] + have h (μν) : ContDiff ℝ n (A.fieldStrengthMatrix · μν) := fieldStrengthMatrix_contDiff hA + fun_prop /-! @@ -448,121 +345,38 @@ lemma kineticTerm_add_time_mul_const {d} {𝓕 : FreeSpace} (A : Electromagnetic have diff_a : ∂_ (Sum.inl 0) (fun x => A x + x (Sum.inl 0) • c) = ∂_ (Sum.inl 0) A + (fun x => c) := by funext x ν - rw [SpaceTime.deriv_eq] - - rw [fderiv_fun_add _ (by fun_prop)] - simp only [Fin.isValue, _root_.add_apply, Lorentz.Vector.apply_add, Pi.add_apply] - congr - rw [fderiv_smul_const (by fun_prop)] - simp [Lorentz.Vector.coordCLM] - exact ha.differentiableAt + rw [SpaceTime.deriv_eq, fderiv_fun_add ha.differentiableAt (by fun_prop), + fderiv_smul_const (by fun_prop)] + simp [Lorentz.Vector.coordCLM, SpaceTime.deriv_eq] have diff_b (i : Fin d) : ∂_ (Sum.inr i) (fun x => A x + x (Sum.inl 0) • c) = ∂_ (Sum.inr i) A := by funext x ν - rw [SpaceTime.deriv_eq] - rw [fderiv_fun_add _ (by fun_prop)] - simp only [Fin.isValue, _root_.add_apply, Lorentz.Vector.apply_add] - rw [fderiv_smul_const (by fun_prop)] - simp only [Fin.isValue, ContinuousLinearMap.smulRight_apply, - Lorentz.Vector.apply_smul] - rw [← SpaceTime.deriv_eq] - simp [Lorentz.Vector.coordCLM] - exact ha.differentiableAt - have hdiff (μ : Fin 1 ⊕ Fin d) : - ∂_ μ (fun x => A x + x (Sum.inl 0) • c) x = - ∂_ μ A x + if μ = Sum.inl 0 then c else 0 := by + rw [SpaceTime.deriv_eq, fderiv_fun_add ha.differentiableAt (by fun_prop), + fderiv_smul_const (by fun_prop)] + simp [Lorentz.Vector.coordCLM, SpaceTime.deriv_eq] + have hdiff (μ ν : Fin 1 ⊕ Fin d) : + ∂_ μ (fun x => A x + x (Sum.inl 0) • c) x ν = + ∂_ μ A x ν + if μ = Sum.inl 0 then c ν else 0 := by match μ with | Sum.inl 0 => simp [diff_a] | Sum.inr i => simp [diff_b i] - rw [kineticTerm_eq_sum_potential] - calc _ - _ = -1 / (2 * 𝓕.μ₀) * - ∑ μ, ∑ ν, (η μ μ * η ν ν * (∂_ μ A x + if μ = Sum.inl 0 then c else 0) ν ^ 2 - - (∂_ μ A x + if μ = Sum.inl 0 then c else 0) ν * - (∂_ ν A x + if ν = Sum.inl 0 then c else 0) μ) := by simp only [hdiff] - _ = -1 / (2 * 𝓕.μ₀) * - ∑ μ, ∑ ν, (η μ μ * η ν ν * (∂_ μ A x ν + if μ = Sum.inl 0 then c ν else 0) ^ 2 - - (∂_ μ A x ν + if μ = Sum.inl 0 then c ν else 0) * - (∂_ ν A x μ + if ν = Sum.inl 0 then c μ else 0)) := by - congr - funext μ - congr - funext ν - congr - all_goals - · simp - split_ifs - simp - rfl - _ = -1 / (2 * 𝓕.μ₀) * - ∑ μ, ∑ ν, ((η μ μ * η ν ν * (∂_ μ A x ν) ^ 2 - ∂_ μ A x ν * ∂_ ν A x μ) + - (if μ = Sum.inl 0 then c ν else 0) * (2 * η μ μ * η ν ν * ∂_ μ A x ν + - η μ μ * η ν ν * (if μ = Sum.inl 0 then c ν else 0) - - (∂_ ν A x μ) - (if ν = Sum.inl 0 then c μ else 0)) - - (∂_ μ A x ν) * (if ν = Sum.inl 0 then c μ else 0)) := by - congr - funext μ - congr - funext ν - ring - _ = -1 / (2 * 𝓕.μ₀) * - ∑ μ, ∑ ν, ((η μ μ * η ν ν * (∂_ μ A x ν) ^ 2 - ∂_ μ A x ν * ∂_ ν A x μ)) + - -1 / (2 * 𝓕.μ₀) * ∑ μ, ∑ ν, ((if μ = Sum.inl 0 then c ν else 0) * - (2 * η μ μ * η ν ν * ∂_ μ A x ν + - η μ μ * η ν ν * (if μ = Sum.inl 0 then c ν else 0) - - (∂_ ν A x μ) - (if ν = Sum.inl 0 then c μ else 0)) - - (∂_ μ A x ν) * (if ν = Sum.inl 0 then c μ else 0)) := by - rw [← mul_add] - rw [← Finset.sum_add_distrib] - congr - funext μ - rw [← Finset.sum_add_distrib] - congr - ring_nf - _ = A.kineticTerm 𝓕 x + - -1 / (2 * 𝓕.μ₀) * ∑ μ, ∑ ν, ((if μ = Sum.inl 0 then c ν else 0) * - (2 * η μ μ * η ν ν * ∂_ μ A x ν + - η μ μ * η ν ν * (if μ = Sum.inl 0 then c ν else 0) - - (∂_ ν A x μ) - (if ν = Sum.inl 0 then c μ else 0)) - - (∂_ μ A x ν) * (if ν = Sum.inl 0 then c μ else 0)) := by - rw [kineticTerm_eq_sum_potential] - _ = A.kineticTerm 𝓕 x + - -1 / (2 * 𝓕.μ₀)* ∑ μ, ∑ ν, ((if μ = Sum.inl 0 then c ν else 0) * - (2 * η μ μ * η ν ν * ∂_ μ A x ν + - η μ μ * η ν ν * (if μ = Sum.inl 0 then c ν else 0) - - (∂_ ν A x μ) - (if ν = Sum.inl 0 then c μ else 0)) - - (∂_ ν A x μ) * (if μ = Sum.inl 0 then c ν else 0)) := by - congr 1 - conv_rhs => - enter [2, 2, μ] - rw [Finset.sum_sub_distrib] - conv_rhs => - rw [Finset.sum_sub_distrib] - enter [2, 2] - rw [Finset.sum_comm] - rw [← Finset.sum_sub_distrib] - conv_rhs => - enter [2, 2, μ] - rw [← Finset.sum_sub_distrib] - _ = A.kineticTerm 𝓕 x + - -1 / (2 * 𝓕.μ₀) * ∑ ν, (c ν * (2 * η ν ν * ∂_ (Sum.inl 0) A x ν + η ν ν * c ν - - (∂_ ν A x (Sum.inl 0)) - (if ν = Sum.inl 0 then c (Sum.inl 0) else 0)) - - (∂_ ν A x (Sum.inl 0)) * c ν) := by - congr 1 - simp - _ = A.kineticTerm 𝓕 x + - -1 / (2 * 𝓕.μ₀) * ∑ ν, ((2 * c ν * η ν ν * ∂_ (Sum.inl 0) A x ν + η ν ν * c ν ^ 2 - - 2 * c ν * (∂_ ν A x (Sum.inl 0))) - c ν * - (if ν = Sum.inl 0 then c (Sum.inl 0) else 0)) := by - congr - funext ν - ring - _ = A.kineticTerm 𝓕 x + - (-1 / (2 * 𝓕.μ₀) * ∑ ν, ((2 * c ν * η ν ν * ∂_ (Sum.inl 0) A x ν + η ν ν * c ν ^ 2 - - 2 * c ν * (∂_ ν A x (Sum.inl 0)))) + 1/(2 * 𝓕.μ₀) * c (Sum.inl 0) ^2) := by - simp only [Fin.isValue, mul_ite, mul_zero, Finset.sum_sub_distrib, Finset.sum_ite_eq', - Finset.mem_univ, ↓reduceIte, one_div, add_right_inj] - ring + rw [kineticTerm_eq_sum_potential, kineticTerm_eq_sum_potential] + simp only [hdiff] + have key (μ ν : Fin 1 ⊕ Fin d) : + η μ μ * η ν ν * (∂_ μ A x ν + if μ = Sum.inl 0 then c ν else 0) ^ 2 - + (∂_ μ A x ν + if μ = Sum.inl 0 then c ν else 0) * + (∂_ ν A x μ + if ν = Sum.inl 0 then c μ else 0) = + (η μ μ * η ν ν * ∂_ μ A x ν ^ 2 - ∂_ μ A x ν * ∂_ ν A x μ) + + ((if μ = Sum.inl 0 then 2 * (c ν * η μ μ * η ν ν * ∂_ μ A x ν) + + η μ μ * η ν ν * c ν ^ 2 - c ν * ∂_ ν A x μ else 0) - + (if ν = Sum.inl 0 then c μ * ∂_ μ A x ν else 0) - + (if μ = Sum.inl 0 then c ν else 0) * (if ν = Sum.inl 0 then c μ else 0)) := by + split_ifs <;> ring + simp only [key] + simp only [Finset.sum_add_distrib, Finset.sum_sub_distrib, Finset.sum_ite_irrel, + Finset.sum_const_zero, Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte, mul_ite, ite_mul, + mul_zero, zero_mul, inl_0_inl_0, one_mul, mul_one, two_mul, add_mul, mul_add] + ring /-! @@ -610,40 +424,25 @@ lemma gradKineticTerm_eq_sum_fderiv {d} {𝓕 : FreeSpace} (A : ElectromagneticP let F : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) → (SpaceTime d → Lorentz.Vector d) → SpaceTime d → ℝ := fun (μ, ν) A' x => (η μ μ * η ν ν * ∂_ μ A' x ν ^ 2 - ∂_ μ A' x ν * ∂_ ν A' x μ) - let F' : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) → (SpaceTime d → ℝ) → - SpaceTime d → Lorentz.Vector d := fun μν => (fun ψ x => - -(fderiv ℝ (fun x' => (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x' * ∂_ μν.1 A x' μν.2) x) - (Lorentz.Vector.basis μν.1) • - Lorentz.Vector.basis μν.2 + - -(fderiv ℝ (fun x' => ∂_ μν.1 A x' μν.2 * - (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x') x) - (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + - -(-(fderiv ℝ (fun x' => ψ x' * ∂_ μν.2 A x' μν.1) x) (Lorentz.Vector.basis μν.1) • - Lorentz.Vector.basis μν.2 + - -(fderiv ℝ (fun x' => ∂_ μν.1 A x' μν.2 * ψ x') x) (Lorentz.Vector.basis μν.2) • - Lorentz.Vector.basis μν.1)) - have F_hasVarAdjDerivAt (μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)) : - HasVarAdjDerivAt (F μν) (F' μν) A := by - have h1 := - HasVarAdjDerivAt.mul _ _ _ _ A (deriv_hasVarAdjDerivAt μν.1 μν.2 A hA) - (deriv_hasVarAdjDerivAt μν.1 μν.2 A hA) - have h1' := HasVarAdjDerivAt.const_mul _ _ A h1 (c := η μν.1 μν.1 * η μν.2 μν.2) - have h2 := - HasVarAdjDerivAt.mul _ _ _ _ A (deriv_hasVarAdjDerivAt μν.1 μν.2 A hA) - (deriv_hasVarAdjDerivAt μν.2 μν.1 A hA) - have h3 := HasVarAdjDerivAt.neg _ _ A h2 - have h4 := HasVarAdjDerivAt.add _ _ _ _ _ h1' h3 - convert h4 - simp [F] - ring - have F_sum_hasVarAdjDerivAt : - HasVarAdjDerivAt (fun A' x => ∑ μ, ∑ ν, F (μ, ν) A' x) (fun ψ x => ∑ μν, F' μν ψ x) A := by - convert HasVarAdjDerivAt.sum _ _ A (hA) (fun i => F_hasVarAdjDerivAt i) - exact Eq.symm (Fintype.sum_prod_type fun x => F x _ _) - have hF_mul := HasVarAdjDerivAt.const_mul _ _ A F_sum_hasVarAdjDerivAt (c := -1/(2 * 𝓕.μ₀)) + have F_h (μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)) := + HasVarAdjDerivAt.congr (G := F μν) + (HasVarAdjDerivAt.add _ _ _ _ _ + (HasVarAdjDerivAt.const_mul _ _ A + (HasVarAdjDerivAt.mul _ _ _ _ A (deriv_hasVarAdjDerivAt μν.1 μν.2 A hA) + (deriv_hasVarAdjDerivAt μν.1 μν.2 A hA)) (c := η μν.1 μν.1 * η μν.2 μν.2)) + (HasVarAdjDerivAt.neg _ _ A + (HasVarAdjDerivAt.mul _ _ _ _ A (deriv_hasVarAdjDerivAt μν.1 μν.2 A hA) + (deriv_hasVarAdjDerivAt μν.2 μν.1 A hA)))) + (fun φ _ => funext fun x => by + simp [F] + ring) + have hF_mul := HasVarAdjDerivAt.const_mul _ _ A + (HasVarAdjDerivAt.congr (G := fun A' x => ∑ μ, ∑ ν, F (μ, ν) A' x) + (HasVarAdjDerivAt.sum _ _ A hA F_h) + (fun φ _ => funext fun x => Fintype.sum_prod_type fun μν => F μν φ x)) + (c := -1/(2 * 𝓕.μ₀)) change HasVarGradientAt (fun A' x => -1 / (2 * 𝓕.μ₀) * ∑ μ, ∑ ν, F (μ, ν) A' x) _ A - apply HasVarGradientAt.intro _ hF_mul - rfl + exact HasVarGradientAt.intro _ hF_mul rfl /-! @@ -671,8 +470,7 @@ lemma gradKineticTerm_eq_sum_sum {d} {𝓕 : FreeSpace} • Lorentz.Vector.basis μ)) := by dsimp rw [Fintype.sum_prod_type] - refine Finset.sum_congr rfl (fun μ _ => ?_) - refine Finset.sum_congr rfl (fun ν _ => ?_) + refine Finset.sum_congr rfl fun μ _ => Finset.sum_congr rfl fun ν _ => ?_ simp only [mul_one, neg_smul, neg_add_rev, neg_neg, mul_neg] ring_nf _ = ∑ (μ : (Fin 1 ⊕ Fin d)), ∑ (ν : (Fin 1 ⊕ Fin d)), @@ -682,13 +480,8 @@ lemma gradKineticTerm_eq_sum_sum {d} {𝓕 : FreeSpace} Lorentz.Vector.basis ν + (fderiv ℝ (fun x' => -1 / (2 * 𝓕.μ₀) * ∂_ μ A x' ν) x) (Lorentz.Vector.basis ν) • Lorentz.Vector.basis μ) := by - apply Finset.sum_congr rfl (fun μ _ => ?_) - apply Finset.sum_congr rfl (fun ν _ => ?_) - rw [← add_smul] - rw [neg_add, ← add_assoc, ← neg_smul, ← add_smul] - congr 1 - · ring_nf - · simp [← neg_smul] + refine Finset.sum_congr rfl fun μ _ => Finset.sum_congr rfl fun ν _ => ?_ + module _ = ∑ (μ : (Fin 1 ⊕ Fin d)), ∑ (ν : (Fin 1 ⊕ Fin d)), ((- 2 * (fderiv ℝ (fun x' => (η μ μ * η ν ν * -1 / (2 * 𝓕.μ₀)) * ∂_ μ A x' ν) x) (Lorentz.Vector.basis μ) + @@ -699,31 +492,17 @@ lemma gradKineticTerm_eq_sum_sum {d} {𝓕 : FreeSpace} conv_lhs => enter [2]; rw [Finset.sum_comm] rw [← Finset.sum_add_distrib] conv_lhs => enter [2, μ]; rw [← Finset.sum_add_distrib] - apply Finset.sum_congr rfl (fun μ _ => ?_) - apply Finset.sum_congr rfl (fun ν _ => ?_) + refine Finset.sum_congr rfl fun μ _ => Finset.sum_congr rfl fun ν _ => ?_ rw [← add_smul] ring_nf - _ = ∑ (μ : (Fin 1 ⊕ Fin d)), ∑ (ν : (Fin 1 ⊕ Fin d)), - ((- 2 * ((η μ μ * η ν ν * -1 / (2 * 𝓕.μ₀)) * ∂_ μ (fun x' => ∂_ μ A x' ν) x) + - 2 * ((-1 / (2 * 𝓕.μ₀) * ∂_ μ (fun x' => ∂_ ν A x' μ) x)))) • Lorentz.Vector.basis ν := by - apply Finset.sum_congr rfl (fun μ _ => ?_) - apply Finset.sum_congr rfl (fun ν _ => ?_) - congr - · rw [fderiv_const_mul] - simp [SpaceTime.deriv_eq] - fun_prop - · rw [fderiv_const_mul] - simp [SpaceTime.deriv_eq] - fun_prop - _ = ∑ (μ : (Fin 1 ⊕ Fin d)), ∑ (ν : (Fin 1 ⊕ Fin d)), - ((1 / (𝓕.μ₀) * (η μ μ * η ν ν * ∂_ μ (fun x' => ∂_ μ A x' ν) x - - ∂_ μ (fun x' => ∂_ ν A x' μ) x)) • Lorentz.Vector.basis ν) := by - apply Finset.sum_congr rfl (fun μ _ => ?_) - apply Finset.sum_congr rfl (fun ν _ => ?_) - ring_nf _ = ∑ (ν : (Fin 1 ⊕ Fin d)), ∑ (μ : (Fin 1 ⊕ Fin d)), (1 / (𝓕.μ₀) * (η μ μ * η ν ν * ∂_ μ (fun x' => ∂_ μ A x' ν) x - - ∂_ μ (fun x' => ∂_ ν A x' μ) x)) • Lorentz.Vector.basis ν := by rw [Finset.sum_comm] + ∂_ μ (fun x' => ∂_ ν A x' μ) x)) • Lorentz.Vector.basis ν := by + rw [Finset.sum_comm] + refine Finset.sum_congr rfl fun ν _ => Finset.sum_congr rfl fun μ _ => ?_ + rw [fderiv_const_mul (by fun_prop), fderiv_const_mul (by fun_prop)] + simp [SpaceTime.deriv_eq] + ring_nf /-! @@ -752,46 +531,21 @@ lemma gradKineticTerm_eq_fieldStrength {d} {𝓕 : FreeSpace} (A : Electromagnet congr 1 ring_nf simp - _ = ∑ (ν : (Fin 1 ⊕ Fin d)), ∑ (μ : (Fin 1 ⊕ Fin d)), - ((1/𝓕.μ₀ * η ν ν) * (∂_ μ (fun x' => η μ μ * ∂_ μ A x' ν) x - - ∂_ μ (fun x' => η ν ν * ∂_ ν A x' μ) x)) • Lorentz.Vector.basis ν := by - apply Finset.sum_congr rfl (fun ν _ => ?_) - apply Finset.sum_congr rfl (fun μ _ => ?_) - congr - · rw [SpaceTime.deriv_eq, SpaceTime.deriv_eq, fderiv_const_mul] - rfl - fun_prop - · rw [SpaceTime.deriv_eq, SpaceTime.deriv_eq, fderiv_const_mul] - rfl - fun_prop - _ = ∑ (ν : (Fin 1 ⊕ Fin d)), ∑ (μ : (Fin 1 ⊕ Fin d)), - ((1/𝓕.μ₀ * η ν ν) * (∂_ μ (fun x' => η μ μ * ∂_ μ A x' ν - - η ν ν * ∂_ ν A x' μ) x)) • Lorentz.Vector.basis ν := by - apply Finset.sum_congr rfl (fun ν _ => ?_) - apply Finset.sum_congr rfl (fun μ _ => ?_) - congr - rw [SpaceTime.deriv_eq, SpaceTime.deriv_eq, SpaceTime.deriv_eq, fderiv_fun_sub] - simp only [FunLike.coe_sub, Pi.sub_apply] - · fun_prop - · fun_prop _ = ∑ (ν : (Fin 1 ⊕ Fin d)), ∑ (μ : (Fin 1 ⊕ Fin d)), ((1/𝓕.μ₀ * η ν ν) * (∂_ μ (A.fieldStrengthMatrix · (μ, ν)) x)) • Lorentz.Vector.basis ν := by - apply Finset.sum_congr rfl (fun ν _ => ?_) - apply Finset.sum_congr rfl (fun μ _ => ?_) - congr - funext x - rw [toFieldStrength_basis_repr_apply_eq_single] - _ = ∑ (ν : (Fin 1 ⊕ Fin d)), ((1/𝓕.μ₀ * η ν ν) * - ∑ (μ : (Fin 1 ⊕ Fin d)), (∂_ μ (A.fieldStrengthMatrix · (μ, ν)) x)) - • Lorentz.Vector.basis ν := by - apply Finset.sum_congr rfl (fun ν _ => ?_) - rw [← Finset.sum_smul, Finset.mul_sum] + refine Finset.sum_congr rfl fun ν _ => Finset.sum_congr rfl fun μ _ => ?_ + congr 2 + conv_rhs => + simp only [toFieldStrength_basis_repr_apply_eq_single] + rw [SpaceTime.deriv_eq, fderiv_fun_sub (by fun_prop) (by fun_prop), + fderiv_const_mul (by fun_prop), fderiv_const_mul (by fun_prop)] + simp [SpaceTime.deriv_eq] _ = ∑ (ν : (Fin 1 ⊕ Fin d)), (1/𝓕.μ₀ * η ν ν) • (∑ (μ : (Fin 1 ⊕ Fin d)), (∂_ μ (A.fieldStrengthMatrix · (μ, ν)) x)) • Lorentz.Vector.basis ν := by apply Finset.sum_congr rfl (fun ν _ => ?_) - rw [smul_smul] + rw [← Finset.sum_smul, ← Finset.mul_sum, ← smul_smul] /-! @@ -811,11 +565,7 @@ lemma gradKineticTerm_eq_electric_magnetic {𝓕 : FreeSpace} (A : Electromagnet ∑ i, (𝓕.μ₀⁻¹ * (1 / 𝓕.c ^ 2 * ∂ₜ (fun t => A.electricField 𝓕.c t x.space) (x.time 𝓕.c) i- ∑ j, Space.deriv j (A.magneticFieldMatrix 𝓕.c (x.time 𝓕.c) · (j, i)) x.space)) • Lorentz.Vector.basis (Sum.inr i) := by - have hdiff (μ ν) : Differentiable ℝ fun x => (A.fieldStrengthMatrix x) (μ, ν) := by - conv => enter [2, x]; rw [toFieldStrength_basis_repr_apply_eq_single] - fun_prop - rw [gradKineticTerm_eq_fieldStrength A x ha] - rw [Fintype.sum_sum_type, Fin.sum_univ_one] + rw [gradKineticTerm_eq_fieldStrength A x ha, Fintype.sum_sum_type, Fin.sum_univ_one] congr 1 · rw [smul_smul] congr 1 @@ -827,8 +577,7 @@ lemma gradKineticTerm_eq_electric_magnetic {𝓕 : FreeSpace} (A : Electromagnet · congr funext j simp only [one_div, inr_i_inr_i, mul_neg, mul_one, neg_smul] - rw [curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix] - rw [smul_smul, ← neg_smul] + rw [curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix, smul_smul, ← neg_smul] congr simp only [one_div, toTimeAndSpace_symm_apply_time_space, sub_add_cancel_left, mul_neg] apply ha.of_le (ENat.LEInfty.out) @@ -842,11 +591,7 @@ lemma gradKineticTerm_eq_electric_magnetic_three {𝓕 : FreeSpace} (A : Electro Space.curl (A.magneticField 𝓕.c (x.time 𝓕.c)) x.space i)) • Lorentz.Vector.basis (Sum.inr i) := by rw [gradKineticTerm_eq_electric_magnetic A x ha] - congr - funext i - congr - rw [magneticField_curl_eq_magneticFieldMatrix] - exact ha.of_le (ENat.LEInfty.out) + simp only [magneticField_curl_eq_magneticFieldMatrix A (ha.of_le ENat.LEInfty.out)] /-! ### B.5. Linearity properties of the variational gradient @@ -857,10 +602,10 @@ lemma gradKineticTerm_add {d} {𝓕 : FreeSpace} (A1 A2 : ElectromagneticPotenti (hA1 : ContDiff ℝ ∞ A1) (hA2 : ContDiff ℝ ∞ A2) : (A1 + A2).gradKineticTerm 𝓕 = A1.gradKineticTerm 𝓕 + A2.gradKineticTerm 𝓕 := by funext x - rw [gradKineticTerm_eq_fieldStrength] + rw [gradKineticTerm_eq_fieldStrength (A1 + A2) x (hA1.add hA2)] simp only [Pi.add_apply] - rw [gradKineticTerm_eq_fieldStrength, gradKineticTerm_eq_fieldStrength] - rw [← Finset.sum_add_distrib] + rw [gradKineticTerm_eq_fieldStrength A1 x hA1, gradKineticTerm_eq_fieldStrength A2 x hA2, + ← Finset.sum_add_distrib] apply Finset.sum_congr rfl (fun ν _ => ?_) rw [← smul_add, ← add_smul, ← Finset.sum_add_distrib] congr @@ -871,22 +616,18 @@ lemma gradKineticTerm_add {d} {𝓕 : FreeSpace} (A1 A2 : ElectromagneticPotenti rw [fieldStrengthMatrix_add _ _ _ (hA1.differentiable (by simp)) (hA2.differentiable (by simp))] simp [Finsupp.coe_add, Pi.add_apply] - rw [fderiv_fun_add] + rw [fderiv_fun_add + (fieldStrengthMatrix_differentiable (hA1.of_le ENat.LEInfty.out)).differentiableAt + (fieldStrengthMatrix_differentiable (hA2.of_le ENat.LEInfty.out)).differentiableAt] rfl - · apply fieldStrengthMatrix_differentiable <| hA1.of_le (ENat.LEInfty.out) - · apply fieldStrengthMatrix_differentiable <| hA2.of_le (ENat.LEInfty.out) - · exact hA2 - · exact hA1 - · exact hA1.add hA2 lemma gradKineticTerm_smul {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (hA : ContDiff ℝ ∞ A) (c : ℝ) : (c • A).gradKineticTerm 𝓕 = c • A.gradKineticTerm 𝓕 := by funext x - rw [gradKineticTerm_eq_fieldStrength] + rw [gradKineticTerm_eq_fieldStrength (c • A) x (hA.const_smul c)] simp only [Pi.smul_apply] - rw [gradKineticTerm_eq_fieldStrength] - rw [Finset.smul_sum] + rw [gradKineticTerm_eq_fieldStrength A x hA, Finset.smul_sum] apply Finset.sum_congr rfl (fun ν _ => ?_) conv_rhs => rw [smul_comm] congr 1 @@ -898,15 +639,12 @@ lemma gradKineticTerm_smul {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential rw [SpaceTime.deriv_eq] change (c • fderiv ℝ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x) (Lorentz.Vector.basis μ) rw [← fderiv_const_smul - (fieldStrengthMatrix_differentiable <| hA.of_le (ENat.LEInfty.out)).differentiableAt] - rw [← SpaceTime.deriv_eq] + (fieldStrengthMatrix_differentiable <| hA.of_le (ENat.LEInfty.out)).differentiableAt, + ← SpaceTime.deriv_eq] congr funext x - rw [fieldStrengthMatrix_smul _ _ _] + rw [fieldStrengthMatrix_smul _ _ _ (hA.differentiable (by simp))] rfl - · exact hA.differentiable (by simp) - · exact hA - · exact hA.const_smul c /-! @@ -925,40 +663,25 @@ lemma kineticTerm_hasVarGradientAt {d} {𝓕 : FreeSpace} (A : ElectromagneticPo let F : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) → (SpaceTime d → Lorentz.Vector d) → SpaceTime d → ℝ := fun (μ, ν) A' x => (η μ μ * η ν ν * ∂_ μ A' x ν ^ 2 - ∂_ μ A' x ν * ∂_ ν A' x μ) - let F' : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) → (SpaceTime d → ℝ) → - SpaceTime d → Lorentz.Vector d := fun μν => (fun ψ x => - -(fderiv ℝ (fun x' => (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x' * ∂_ μν.1 A x' μν.2) x) - (Lorentz.Vector.basis μν.1) • - Lorentz.Vector.basis μν.2 + - -(fderiv ℝ (fun x' => ∂_ μν.1 A x' μν.2 * - (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x') x) - (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + - -(-(fderiv ℝ (fun x' => ψ x' * ∂_ μν.2 A x' μν.1) x) (Lorentz.Vector.basis μν.1) • - Lorentz.Vector.basis μν.2 + - -(fderiv ℝ (fun x' => ∂_ μν.1 A x' μν.2 * ψ x') x) (Lorentz.Vector.basis μν.2) • - Lorentz.Vector.basis μν.1)) - have F_hasVarAdjDerivAt (μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)) : - HasVarAdjDerivAt (F μν) (F' μν) A := by - have h1 := - HasVarAdjDerivAt.mul _ _ _ _ A (deriv_hasVarAdjDerivAt μν.1 μν.2 A hA) - (deriv_hasVarAdjDerivAt μν.1 μν.2 A hA) - have h1' := HasVarAdjDerivAt.const_mul _ _ A h1 (c := η μν.1 μν.1 * η μν.2 μν.2) - have h2 := - HasVarAdjDerivAt.mul _ _ _ _ A (deriv_hasVarAdjDerivAt μν.1 μν.2 A hA) - (deriv_hasVarAdjDerivAt μν.2 μν.1 A hA) - have h3 := HasVarAdjDerivAt.neg _ _ A h2 - have h4 := HasVarAdjDerivAt.add _ _ _ _ _ h1' h3 - convert h4 - simp [F] - ring - have F_sum_hasVarAdjDerivAt : - HasVarAdjDerivAt (fun A' x => ∑ μ, ∑ ν, F (μ, ν) A' x) (fun ψ x => ∑ μν, F' μν ψ x) A := by - convert HasVarAdjDerivAt.sum _ _ A (hA) (fun i => F_hasVarAdjDerivAt i) - exact Eq.symm (Fintype.sum_prod_type fun x => F x _ _) - have hF_mul := HasVarAdjDerivAt.const_mul _ _ A F_sum_hasVarAdjDerivAt (c := -1/(2 * 𝓕.μ₀)) + have F_h (μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)) := + HasVarAdjDerivAt.congr (G := F μν) + (HasVarAdjDerivAt.add _ _ _ _ _ + (HasVarAdjDerivAt.const_mul _ _ A + (HasVarAdjDerivAt.mul _ _ _ _ A (deriv_hasVarAdjDerivAt μν.1 μν.2 A hA) + (deriv_hasVarAdjDerivAt μν.1 μν.2 A hA)) (c := η μν.1 μν.1 * η μν.2 μν.2)) + (HasVarAdjDerivAt.neg _ _ A + (HasVarAdjDerivAt.mul _ _ _ _ A (deriv_hasVarAdjDerivAt μν.1 μν.2 A hA) + (deriv_hasVarAdjDerivAt μν.2 μν.1 A hA)))) + (fun φ _ => funext fun x => by + simp [F] + ring) + have hF_mul := HasVarAdjDerivAt.const_mul _ _ A + (HasVarAdjDerivAt.congr (G := fun A' x => ∑ μ, ∑ ν, F (μ, ν) A' x) + (HasVarAdjDerivAt.sum _ _ A hA F_h) + (fun φ _ => funext fun x => Fintype.sum_prod_type fun μν => F μν φ x)) + (c := -1/(2 * 𝓕.μ₀)) change HasVarGradientAt (fun A' x => -1 / (2 * 𝓕.μ₀) * ∑ μ, ∑ ν, F (μ, ν) A' x) _ A - apply HasVarGradientAt.intro _ hF_mul - rfl + exact HasVarGradientAt.intro _ hF_mul rfl /-! diff --git a/Physlib/QuantumMechanics/DDimensions/Operators/SpectralTheory/Basic.lean b/Physlib/QuantumMechanics/DDimensions/Operators/SpectralTheory/Basic.lean index 38d41d1f2..7554b4634 100644 --- a/Physlib/QuantumMechanics/DDimensions/Operators/SpectralTheory/Basic.lean +++ b/Physlib/QuantumMechanics/DDimensions/Operators/SpectralTheory/Basic.lean @@ -115,9 +115,8 @@ scoped notation "𝑅" => resolvent def IsLowerBound (T : H →ₗ.[ℂ] H) (z : ℂ) (c : ℝ) : Prop := ∀ x : T.domain, c * ‖x‖ ≤ ‖T x - z • x‖ lemma isLowerBound_neg {T : H →ₗ.[ℂ] H} {z : ℂ} {c : ℝ} (h : IsLowerBound T z c) : - IsLowerBound (-T) (-z) c := by - intro x - simp only [neg_apply, neg_smul, sub_neg_eq_add, norm_neg_add, h x] + IsLowerBound (-T) (-z) c := + fun x ↦ by simpa [neg_apply, norm_neg_add] using h x lemma isLowerBound_of_right_le {T : H →ₗ.[ℂ] H} {z : ℂ} {c₁ c₂ : ℝ} (hle : c₁ ≤ c₂) (h : IsLowerBound T z c₂) : @@ -136,9 +135,8 @@ lemma isLowerBound_closure obtain ⟨b, hb, hb'⟩ := mem_closure_iff_seq_limit.mp <| hT.graph_closure_eq_closure_graph ▸ T.closure.mem_graph x rw [nhds_prod_eq] at hb' - have hb₁ := hb'.fst.norm.const_mul c - have hb₂ := (hb'.snd.sub <| hb'.fst.const_smul z).norm - refine le_of_tendsto_of_tendsto' hb₁ hb₂ fun n ↦ ?_ + refine le_of_tendsto_of_tendsto' (hb'.fst.norm.const_mul c) + ((hb'.snd.sub <| hb'.fst.const_smul z).norm) fun n ↦ ?_ obtain ⟨y, hy₁, hy₂⟩ := (mem_graph_iff _).mp (hb n) exact hy₁ ▸ hy₂ ▸ h y · rwa [closure_def' hT] @@ -224,9 +222,9 @@ lemma regularityDomain_isOpen (T : H →ₗ.[ℂ] H) : IsOpen T.regularityDomain /-- `T` and `T.closure` have the same regularity domain. -/ lemma regularityDomain_closure (T : H →ₗ.[ℂ] H) : - T.closure.regularityDomain = T.regularityDomain := by - refine eq_of_le_of_ge (regularityDomain_antitone T.le_closure) ?_ - exact fun _ ⟨c, hc, h⟩ ↦ ⟨c, hc, isLowerBound_closure h⟩ + T.closure.regularityDomain = T.regularityDomain := + eq_of_le_of_ge (regularityDomain_antitone T.le_closure) + fun _ ⟨c, hc, h⟩ ↦ ⟨c, hc, isLowerBound_closure h⟩ lemma IsClosable.closure_range_sub_eq_range_closure_sub [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hT : T.IsClosable) {z : ℂ} (hz : z ∈ T.regularityDomain) : @@ -271,9 +269,9 @@ lemma IsClosable.closure_range_sub_eq_range_closure_sub [CompleteSpace H] lemma IsClosed.sub_range_isClosed [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hT : T.IsClosed) {z : ℂ} (hz : z ∈ T.regularityDomain) : - _root_.IsClosed ((T - z • 1).toFun.range : Set H) := by - have hT' : T.closure = T := hT.isClosable.isClosed_iff.mp hT - exact (hT' ▸ hT.isClosable.closure_range_sub_eq_range_closure_sub hz) ▸ isClosed_closure + _root_.IsClosed ((T - z • 1).toFun.range : Set H) := + (hT.isClosable.isClosed_iff.mp hT ▸ + hT.isClosable.closure_range_sub_eq_range_closure_sub hz) ▸ isClosed_closure /-- `(T.closure - z • 1).rangeᗮ = (T† - conj z • 1).ker` -/ lemma IsUnbounded.orthogonal_closure_sub_range [CompleteSpace H] @@ -344,8 +342,7 @@ lemma IsClosed.defectNumber_eq_zero_iff [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hT : T.IsClosed) {z : ℂ} (hz : z ∈ T.regularityDomain) : T.defectNumber z = 0 ↔ (T - z • 1).toFun.range = ⊤ := by haveI := hT.sub_range_isClosed hz -- needed for HasOrthogonalProjection - rw [← orthogonal_eq_bot_iff, ← rank_eq_zero] - exact Iff.rfl + exact rank_eq_zero.trans orthogonal_eq_bot_iff /-- `T` and `T.closure` have the same defect number at points in their regularity domain. -/ lemma defectNumber_closure [CompleteSpace H] @@ -408,8 +405,7 @@ lemma IsClosable.defectNumber_eq_of_mem_ball [CompleteSpace H] {T : H →ₗ.[ · simp [sub_smul, pow_two] rw [inner_sub_left, h', zero_sub, inner_smul_left, norm_neg, norm_mul, norm_conj, mul_assoc] exact mul_le_mul_of_nonneg_left (norm_inner_le_norm _ _) (norm_nonneg _) - · false_or_by_contra -- `z₁ ∉ T.regularityDomain` ⇒ `c ≤ 0` ⇒ `z₂ ∈ ∅` - exact hz₁ ⟨c, lt_of_le_of_lt dist_nonneg h_ball, h⟩ + · exact absurd ⟨c, dist_nonneg.trans_lt h_ball, h⟩ hz₁ /-- The defect number is constant on each connected component of the regularity domain. -/ lemma IsClosable.defectNumber_const [CompleteSpace H] @@ -469,8 +465,7 @@ lemma IsClosable.defectNumber_const [CompleteSpace H] apply h₁' ▸ h₂' rw [← defectNumber_eq_of_mem_ball hT hc_bound (hε_ball h₁)] rw [← defectNumber_eq_of_mem_ball hT hc_bound (hε_ball h₂)] - · false_or_by_contra - exact (mem_empty_iff_false z₂).mp (connectedComponentIn_eq_empty hz₁ ▸ hz) + · exact ((mem_empty_iff_false z₂).mp (connectedComponentIn_eq_empty hz₁ ▸ hz)).elim /-! ## C. Numerical range @@ -492,8 +487,7 @@ lemma mem_numericalRange {T : H →ₗ.[ℂ] H} {x : T.domain} (hx : x ≠ 0) : lemma numericalRange_nonempty {T : H →ₗ.[ℂ] H} (hT : T.domain ≠ ⊥) : (Θ T).Nonempty := by obtain ⟨x, hx, hx'⟩ := exists_mem_ne_zero_of_ne_bot hT - use (‖x‖ ^ 2)⁻¹ * ⟪x, T ⟨x, hx⟩⟫_ℂ - exact mem_numericalRange (x := ⟨x, hx⟩) (Subtype.coe_ne_coe.mp hx') + exact ⟨_, mem_numericalRange (x := ⟨x, hx⟩) (Subtype.coe_ne_coe.mp hx')⟩ @[simp] lemma numericalRange_neg (T : H →ₗ.[ℂ] H) : Θ (-T) = -Θ T := by @@ -664,9 +658,7 @@ lemma mem_resolventSet_iff {T : H →ₗ.[ℂ] H} {z : ℂ} : /-- If an operator is not closed then its resolvent set is empty. -/ lemma resolventSet_eq_empty [CompleteSpace H] {T : H →ₗ.[ℂ] H} (h : ¬T.IsClosed) : ρ T = ∅ := by - ext z - simp only [mem_empty_iff_false, iff_false] - by_contra ⟨h_ker, h_range, h_cont⟩ + refine eq_empty_iff_forall_notMem.mpr fun z ⟨h_ker, h_range, h_cont⟩ ↦ ?_ suffices (T - z • 1).IsClosed by have hTz : T - z • 1 + z • 1 = T := eq_of_le_of_domain_eq (sub_add_le_cancel _ _) (by simp [add_domain, sub_domain]) @@ -695,12 +687,10 @@ lemma IsClosed.resolventSet_eq [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hT : T. lemma IsClosed.resolventSet_eq' [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hT : T.IsClosed) : ρ T = T.regularityDomain ∩ T.defectNumber ⁻¹' {0} := by ext z - constructor - · intro hρ - have hz : z ∈ T.regularityDomain := T.resolventSet_subset_regularityDomain hρ + refine ⟨fun hρ ↦ ?_, fun ⟨h_reg, h_defect⟩ ↦ ?_⟩ + · have hz : z ∈ T.regularityDomain := T.resolventSet_subset_regularityDomain hρ exact ⟨hz, (hT.defectNumber_eq_zero_iff hz).mpr hρ.2.1⟩ - · intro ⟨h_reg, h_defect⟩ - obtain ⟨h_ker, h_cont⟩ := mem_regularityDomain_iff.mp h_reg + · obtain ⟨h_ker, h_cont⟩ := mem_regularityDomain_iff.mp h_reg exact ⟨h_ker, (hT.defectNumber_eq_zero_iff h_reg).mp h_defect, h_cont⟩ /-- The resolvent set is an open subset of ℂ. -/ @@ -734,8 +724,7 @@ lemma spectrum_eq (T : H →ₗ.[ℂ] H) : σ T = (ρ T)ᶜ := rfl lemma mem_spectrum_iff {T : H →ₗ.[ℂ] H} {z : ℂ} : z ∈ σ T ↔ (T - z • 1).toFun.ker ≠ ⊥ ∨ (T - z • 1).toFun.range ≠ ⊤ ∨ ¬Continuous (𝑅 T z) := by - rw [spectrum_eq, mem_compl_iff, mem_resolventSet_iff] - tauto + simp only [spectrum_eq, mem_compl_iff, mem_resolventSet_iff, not_and_or, ne_eq] /-- If an operator is not closed then its spectrum is all of ℂ. -/ lemma spectrum_eq_univ [CompleteSpace H] {T : H →ₗ.[ℂ] H} (h : ¬T.IsClosed) : σ T = univ := @@ -836,10 +825,8 @@ lemma IsClosed.spectrum_eq [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hT : T.IsCl · refine union_subset ?_ T.continuousSpectrum_subset_spectrum exact union_subset T.pointSpectrum_subset_spectrum T.residualSpectrum_subset_spectrum -lemma pointSpectrum_inter_residualSpectrum (T : H →ₗ.[ℂ] H) : σᵖ T ∩ σʳ T = ∅ := by - ext - simp only [mem_inter_iff, mem_empty_iff_false, iff_false, not_and] - exact fun h h' ↦ h h'.1 +lemma pointSpectrum_inter_residualSpectrum (T : H →ₗ.[ℂ] H) : σᵖ T ∩ σʳ T = ∅ := + eq_empty_iff_forall_notMem.mpr fun _ ⟨h, h'⟩ ↦ h h'.1 /-! ## E. Resolvent identities