Source indexedlemma · leanprover/lean4:v4.32.0

RS.SumDiff.sum_le_sumAbsDiff_of_points_subset

PrimeNumberTheoremAnd.Unused.MyMV_A3a · PrimeNumberTheoremAnd/Unused/MyMV_A3a.lean:686 to 724

Source documentation

Sum of absolute increments of g over an untagged partition. -/ def sumAbsDiff {a b : ℝ} (g : ℝ → ℝ) (P : IPart.IPartition a b) : ℝ := ∑ i : Fin P.n, |g (P.x i.succ) - g (P.x i.castSucc)|

/- The absolute difference of g over a subinterval of P is bounded by the sum of absolute differences of g over the corresponding subintervals of R. -/ lemma sumAbsDiff_block_le {a b : ℝ} {g : ℝ → ℝ} {P R : IPart.IPartition a b} (k : Fin (P.n + 1) → Fin (R.n + 1)) (hk : Monotone k) (hk_eq : ∀ i, R.x (k i) = P.x i) (i : Fin P.n) : |g (P.x i.succ) - g (P.x i.castSucc)| ≤ ∑ j ∈ Finset.Ico (k i.castSucc).val (k i.succ).val, |IPart.term g R j| := by rw [← hk_eq i.succ, ← hk_eq i.castSucc] rw [← IPart.sum_telescope_block g R (k i.castSucc) (k i.succ) (hk (Nat.le_succ _))] apply Finset.abs_sum_le_sum_abs

/- sumAbsDiff is monotonic with respect to partition refinement. -/ lemma sumAbsDiff_mono_of_refinement {a b : ℝ} {g : ℝ → ℝ} {P R : IPart.IPartition a b} (hPR : IPart.IsRefinement R P) : sumAbsDiff g P ≤ sumAbsDiff g R := by -- Use refinement_index_map to get k. obtain ⟨k, , hk_eq⟩ : ∃ k : Fin (P.n + 1) → Fin (R.n + 1), Monotone k ∧ ∀ i, R.x (k i) = P.x i := by exact IPart.refinement_index_map P R hPR; -- Apply sumAbsDiff_block_le to bound the sum over P by the double sum over blocks of R. have h_sum_le_double_sum : ∑ i : Fin P.n, |g (P.x i.succ) - g (P.x i.castSucc)| ≤ ∑ i : Fin P.n, ∑ j ∈ Finset.Ico (k i.castSucc).val (k i.succ).val, |IPart.term g R j| := by exact Finset.sum_le_sum fun i _ => sumAbsDiff_block_le k ‹› ‹_› i; -- Use sum_partition_blocks to collapse the double sum into a single sum over Ico (k 0) (k P.n). have h_double_sum_to_single_sum : ∑ i : Fin P.n, ∑ j ∈ Finset.Ico (k i.castSucc).val (k i.succ).val, |IPart.term g R j| = ∑ j ∈ Finset.Ico (k 0).val (k (Fin.last P.n)).val, |IPart.term g R j| := by have h_double_sum_to_single_sum : ∀ (n : ℕ) (k : Fin (n + 1) → ℕ) (hk : Monotone k), ∑ i : Fin n, ∑ j ∈ Finset.Ico (k i.castSucc) (k i.succ), |IPart.term g R j| = ∑ j ∈ Finset.Ico (k 0) (k (Fin.last n)), |IPart.term g R j| := by exact fun n k hk ↦ IPart.sum_partition_blocks n k hk fun j ↦ |IPart.term g R j|; convert h_double_sum_to_single_sum P.n ( fun i => ( k i : ℕ ) ) ( fun i j hij => by simpa using ‹Monotone k› hij ) using 1; -- Bound this sum by the sum over range R.n (since terms are non-negative and the interval is a subset). have h_single_sum_le_range : ∑ j ∈ Finset.Ico (k 0).val (k (Fin.last P.n)).val, |IPart.term g R j| ≤ ∑ j ∈ Finset.Ico 0 R.n, |IPart.term g R j| := by refine' Finset.sum_le_sum_of_subset_of_nonneg _ fun _ _ _ => abs_nonneg _; refine' Finset.Ico_subset_Ico _ _ <;> norm_num; exact Nat.le_of_lt_succ ( Fin.is_lt _ ); convert h_sum_le_double_sum.trans ( h_double_sum_to_single_sum.le.trans h_single_sum_le_range ) using 1; simp +decide [ sumAbsDiff, Finset.sum_range, Fin.cast_val_eq_self ]; refine' Finset.sum_congr rfl fun i hi => _ ; unfold IPart.term ; aesop

/- sumAbsDiff is monotonic with respect to partition refinement. -/ lemma sumAbsDiff_le_sumAbsDiff_of_refinement {a b : ℝ} {g : ℝ → ℝ} {P R : IPart.IPartition a b} (hPR : IPart.IsRefinement R P) : sumAbsDiff g P ≤ sumAbsDiff g R := by convert sumAbsDiff_mono_of_refinement hPR using 1

/- If x is a monotone sequence of points contained in partition P, then the sum of absolute differences of g along x is bounded by sumAbsDiff g P.

Exact Lean statement

lemma sum_le_sumAbsDiff_of_points_subset {a b : ℝ} (g : ℝ → ℝ) (P : RS.IPart.IPartition a b)
    (p : ℕ) (x : Fin (p + 1) → ℝ) (hx : Monotone x)
    (h_subset : ∀ i, x i ∈ P.points) :
    ∑ i : Fin p, |g (x i.succ) - g (x i.castSucc)| ≤ RS.SumDiff.sumAbsDiff g P

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma sum_le_sumAbsDiff_of_points_subset {a b : ℝ} (g : ℝ → ℝ) (P : RS.IPart.IPartition a b)    (p : ℕ) (x : Fin (p + 1) → ℝ) (hx : Monotone x)    (h_subset : ∀ i, x i ∈ P.points) :    ∑ i : Fin p, |g (x i.succ) - g (x i.castSucc)| ≤ RS.SumDiff.sumAbsDiff g P := by      -- By definition of $P.points$, there exists a monotone map $k : Fin (p + 1) → Fin (P.n + 1)$ such that $P.x (k i) = x i$ for all $i$.      obtain ⟨k, hk⟩ : ∃ k : Fin (p + 1) → Fin (P.n + 1), Monotone k ∧ ∀ i : Fin (p + 1), P.x (k i) = x i := by        -- By definition of $P.points$, there exists a monotone map $k : Fin (p + 1) → Fin (P.n + 1)$ such that $P.x (k i) = x i$ for all $i$ by the properties of the points of $P$.        have h_k_exists : ∀ y ∈ P.points, ∃ i : Fin (P.n + 1), P.x i = y := by          exact fun y hy => by rw [ IPart.IPartition.points ] at hy; aesop;        choose k hk using h_k_exists;        use fun i => k ( x i ) ( h_subset i );        have h_k_mono : ∀ i j : Fin (p + 1), x i ≤ x j → k (x i) (h_subset i) ≤ k (x j) (h_subset j) := by          intros i j hij          have h_k_mono : P.x (k (x i) (h_subset i)) ≤ P.x (k (x j) (h_subset j)) := by            aesop;          contrapose! h_k_mono;          apply_rules [ P.monotone, lt_of_le_of_ne ];          · exact le_of_lt h_k_mono;          · grind;        exact ⟨ fun i j hij => h_k_mono i j <| hx hij, fun i => hk _ _ ⟩;      -- Apply the lemma `sum_telescope_abs_le` to each term in the sum.      have h_telescope : ∀ i : Fin p, |g (x (i.succ)) - g (x (i.castSucc))| ≤ ∑ j ∈ Finset.Ico (k (i.castSucc)).val (k (i.succ)).val, |RS.IPart.term g P j| := by        intros i        have h_telescope : |g (P.x (k (i.succ))) - g (P.x (k (i.castSucc)))| ≤ ∑ j ∈ Finset.Ico (k (i.castSucc)).val (k (i.succ)).val, |RS.IPart.term g P j| := by          convert IPart.sum_telescope_abs_le g P ( k ( Fin.castSucc i ) ) ( k ( Fin.succ i ) ) _ using 1;          exact hk.1 ( Nat.le_succ _ );        aesop;      -- Apply the lemma `sum_partition_blocks` to combine the sums over the intervals `[k i, k (i+1))`.      have h_sum_partition_blocks : ∑ i : Fin p, ∑ j ∈ Finset.Ico (k (i.castSucc)).val (k (i.succ)).val, |RS.IPart.term g P j| ≤ ∑ j ∈ Finset.Ico (k 0).val (k (Fin.last p)).val, |RS.IPart.term g P j| := by        have h_sum_partition_blocks : ∑ i : Fin p, ∑ j ∈ Finset.Ico (k (i.castSucc)).val (k (i.succ)).val, |RS.IPart.term g P j| = ∑ j ∈ Finset.Ico (k 0).val (k (Fin.last p)).val, |RS.IPart.term g P j| := by          convert RS.IPart.sum_partition_blocks p ( fun i => ( k i : ℕ ) ) hk.1 _ using 1;        grind;      refine le_trans ( Finset.sum_le_sum fun i _ => h_telescope i ) ( h_sum_partition_blocks.trans ?_ );      refine' le_trans ( Finset.sum_le_sum_of_subset_of_nonneg ( Finset.subset_iff.mpr _ ) fun _ _ _ => abs_nonneg _ ) _;      exact Finset.range P.n;      · simp +zetaDelta at *;        intro i hi₁ hi₂; exact lt_of_lt_of_le hi₂ ( Nat.le_of_lt_succ <| by simp [ Fin.is_lt ] ) ;      · simp +decide [ Finset.sum_range, IPart.term ];        rfl