Finish the proof!

leanprover-community · Aug 5, 2019 · f7be6ab · f7be6ab
1 parent b863bf8
commit f7be6ab
Showing 1 changed file with 11 additions and 11 deletions.
diff --git a/src/sensitivity.lean b/src/sensitivity.lean
@@ -459,7 +459,7 @@ begin
     rcases finset.mem_image.1 (finset.mem_of_max hx) with ⟨q, hq, rfl⟩,
     use q,
     refine ⟨set.mem_to_finset.1 hq, λ q' hq', _⟩,
-    exact (finset.le_max_of_mem (finset.mem_image_of_mem _ (set.mem_to_finset.2 hq')) hx : _) }, -- get q by finset.sup?
+    exact (finset.le_max_of_mem (finset.mem_image_of_mem _ (set.mem_to_finset.2 hq')) hx : _) },
   have H_q_pos : 0 < abs (l q),
   { rw [abs_pos_iff],
     assume h,
@@ -478,16 +478,16 @@ begin
     by { exact (mul_le_mul_right H_q_pos).mp ‹_› },
   rw [← abs_sqrt_nat, ← abs_mul],
   transitivity abs (ε q (real.sqrt (↑m + 1) • y)),
-    { rw [linear_map.map_smul, smul_eq_mul, abs_mul, abs_mul],
-      apply mul_le_mul_of_nonneg_left _ _,
-      { apply le_of_eq, congr' 1, rw [← H_l₂, finsupp.total_apply, finsupp.sum, linear_map.map_sum],
-        rw [finset.sum_eq_single q],
-        { rw [linear_map.map_smul, smul_eq_mul, duality, if_pos rfl, mul_one], },
-        { intros p hp hne, sorry },
-        { sorry },
-      },
-      { exact abs_nonneg _ }
-      },
+  { rw [linear_map.map_smul, smul_eq_mul, abs_mul, abs_mul],
+    apply mul_le_mul_of_nonneg_left _ _,
+    { apply le_of_eq, congr' 1, rw [← H_l₂, finsupp.total_apply, finsupp.sum, linear_map.map_sum],
+      rw [finset.sum_eq_single q],
+      { rw [linear_map.map_smul, smul_eq_mul, duality, if_pos rfl, mul_one], },
+      { intros p hp hne, 
+        simp [linear_map.map_smul, duality, hne.symm] },
+      { intro h_q_ne_supp,
+        simp [finsupp.not_mem_support_iff.mp h_q_ne_supp] } },
+    { exact abs_nonneg _ } },
   rw [← f_image_g y (by simpa using H_mem''), ← H_l₂, finsupp.total_apply, finsupp.sum,
       linear_map.map_sum, linear_map.map_sum],
   refine le_trans abs_triangle_sum _,