Source indexedlemma · leanprover/lean4:v4.32.0

RS.SumDiff.sumAbsDiff_mono_of_refinement

PrimeNumberTheoremAnd.Unused.MyMV_A3a · PrimeNumberTheoremAnd/Unused/MyMV_A3a.lean:650 to 672

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.

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

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