Mathlib.Analysis.Quantization
Paired weighted scalar L1 quantization on a compact real interval.
Core 5 core · 5 supporting Finite paired weighted scalar quantization: measurable partitions, cost, and compact regularity of the coefficients. ★ sqrt_mass_regular
Finite paired weighted scalar quantization: measurable partitions, cost, and compact regularity of the coefficients. The cells in this module may be disconnected.
abbrev IsMeasurablePartition reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Quantization
A family of k cells is a measurable partition of the closed source interval from a to b when its cells are measurable, pairwise disjoint, and their union is exactly that interval. No cell is required to be an interval. This is the real-line instance of the library's finite measurable partition predicate IsIntervalPartition.
Definition (Lean source)
def weightedCost reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Quantization
The paired weighted absolute-deviation cost of a family of k cells B_j and reproduction points z_(j,s), for S coefficient functions β_s, is the sum over cells j and coefficients s of the integral over x in B_j of β_s(x, z_(j,s))·|x − z_(j,s)|. One common cell partition is used for all coefficients, with a separate reproduction point for each coefficient in each cell.
def optimalCost reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Quantization
The optimal paired cost on the source interval from a to b with k cells is the infimum of the paired weighted cost over every measurable partition of that interval into k cells and every array of reproduction points lying in the interval. When no such partition exists or the costs are unbounded below, the infimum is read as zero.
Definition (Lean source)
parameters
def
optimalCost a b S k β :
ℝ
given by
sInf {v : ℝ | ∃ (B : Fin k → Set ℝ) (z : Fin k → Fin S → ℝ), IsMeasurablePartition a b k B ∧ (∀ j s, z j s ∈ Icc a b) ∧ v = weightedCost S k β B z}
def diagonalWeight reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Quantization
The diagonal density is the sum of the coefficients evaluated at the same source and reproduction point.
theorem sqrt_mass_regular reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Quantization
On the interval endpoints with strict positive length, a nonempty finite family of loss weights that are jointly continuous and strictly positive has a continuous square-root diagonal density with positive total mass.
Formal statement
hypotheses
Proof (Lean source)
theorem sqrt_mass_regular (a b : ℝ) (hab : a < b) (S : ℕ) (hS : 0 < S)
(β : Fin S → ℝ → ℝ → ℝ)
(hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2)
(Icc a b ×ˢ Icc a b))
(hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z) :
ContinuousOn (fun x => sqrt (diagonalWeight S β x)) (Icc a b) ∧
0 < ∫ x in a..b, sqrt (diagonalWeight S β x) := by
-- Use diagonal_regular, positive compact minimum, and integral positivity.
obtain ⟨hc, hp⟩ := diagonal_regular a b S hS β hcont hpos
have hroot : ContinuousOn (fun x => sqrt (diagonalWeight S β x))
(Icc a b) := Real.continuous_sqrt.comp_continuousOn hc
refine ⟨hroot, intervalIntegral.integral_pos hab hroot ?_ ?_⟩
· intro x hx
exact (Real.sqrt_nonneg _)
· refine ⟨a, ⟨le_refl a, le_of_lt hab⟩, ?_⟩
exact Real.sqrt_pos.2 (hp a ⟨le_refl a, le_of_lt hab⟩)
5 supporting declarations (lemmas, instances)
-
coefficient_boundstheorem — All members of a finite family of continuous positive coefficients have one strictly positive lower bound and one finite upper bound on the square.hypothesesa b :ℝhab :a < bS :ℕhS :0 < Sβ :Fin S → ℝ → ℝ → ℝhcont :∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2) (Set.Icc a b ×ˢ Set.Icc a b)hpos :∀ s x zifx ∈ Set.Icc a bandz ∈ Set.Icc a bthen0 < β s x zconclusion∃ c C : ℝ,0 < cconclusion 1s :x ∈ Set.Icc a b :z ∈ Set.Icc a b :c ≤ β s x zβ s x z ≤ CProof (Lean source)
theorem coefficient_bounds (a b : ℝ) (hab : a < b) (S : ℕ) (hS : 0 < S) (β : Fin S → ℝ → ℝ → ℝ) (hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2) (Set.Icc a b ×ˢ Set.Icc a b)) (hpos : ∀ s x z, x ∈ Set.Icc a b → z ∈ Set.Icc a b → 0 < β s x z) : ∃ c C : ℝ, 0 < c ∧ ∀ s, ∀ x ∈ Set.Icc a b, ∀ z ∈ Set.Icc a b, c ≤ β s x z ∧ β s x z ≤ C := by -- Apply compact extrema on the square for each index and take finite min/max. classical let K : Set (ℝ × ℝ) := Set.Icc a b ×ˢ Set.Icc a b have hK : IsCompact K := isCompact_Icc.prod isCompact_Icc have hKn : K.Nonempty := ⟨(a, a), ⟨⟨le_refl a, le_of_lt hab⟩, ⟨le_refl a, le_of_lt hab⟩⟩⟩ have hlocal (s : Fin S) : ∃ c C : ℝ, 0 < c ∧ ∀ x ∈ Set.Icc a b, ∀ z ∈ Set.Icc a b, c ≤ β s x z ∧ β s x z ≤ C := by obtain ⟨p, hp, hmin⟩ := hK.exists_isMinOn hKn (hcont s) obtain ⟨q, hq, hmax⟩ := hK.exists_isMaxOn hKn (hcont s) refine ⟨β s p.1 p.2, β s q.1 q.2, hpos s p.1 p.2 hp.1 hp.2, ?_⟩ intro x hx z hz have hmem : (x, z) ∈ K := ⟨hx, hz⟩ exact ⟨hmin hmem, hmax hmem⟩ choose c C hc using hlocal let : Nonempty (Fin S) := ⟨⟨0, hS⟩⟩ obtain ⟨i, hi⟩ := Finite.exists_min c obtain ⟨j, hj⟩ := Finite.exists_max C refine ⟨c i, C j, (hc i).1, ?_⟩ intro s x hx z hz obtain ⟨hl, hu⟩ := (hc s).2 x hx z hz exact ⟨(hi s).trans hl, hu.trans (hj s)⟩ -
coefficient_uniform_continuitytheorem — Joint continuity on the compact square is uniform across the finite family. Here closeness of pairs uses the product metric.hypothesesProof (Lean source)
theorem coefficient_uniform_continuity (a b : ℝ) (S : ℕ) (β : Fin S → ℝ → ℝ → ℝ) (hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2) (Icc a b ×ˢ Icc a b)) : ∀ ε : ℝ, 0 < ε → ∃ δ : ℝ, 0 < δ ∧ ∀ s (p q : ℝ × ℝ), p ∈ Icc a b ×ˢ Icc a b → q ∈ Icc a b ×ˢ Icc a b → dist p q < δ → |β s p.1 p.2 - β s q.1 q.2| < ε := by -- Heine-Cantor for each index, followed by a finite minimum of the radii. classical intro ε hε by_cases hS : 0 < S · have hlocal (s : Fin S) : ∃ δ : ℝ, 0 < δ ∧ ∀ (p q : ℝ × ℝ), p ∈ Icc a b ×ˢ Icc a b → q ∈ Icc a b ×ˢ Icc a b → dist p q < δ → |β s p.1 p.2 - β s q.1 q.2| < ε := by have hu := (isCompact_Icc.prod isCompact_Icc).uniformContinuousOn_of_continuous (hcont s) obtain ⟨δ, hδ, hd⟩ := (Metric.uniformContinuousOn_iff.mp hu) ε hε refine ⟨δ, hδ, ?_⟩ intro p q hp hq hpq simpa [Real.dist_eq] using hd p hp q hq hpq choose d hd using hlocal let : Nonempty (Fin S) := ⟨⟨0, hS⟩⟩ obtain ⟨i, hi⟩ := Finite.exists_min d refine ⟨d i, (hd i).1, ?_⟩ intro s p q hp hq hpq exact (hd s).2 p q hp hq (lt_of_lt_of_le hpq (hi s)) · have hzero : S = 0 := Nat.eq_zero_of_not_pos hS subst S refine ⟨1, by norm_num, ?_⟩ intro s exact elim0 s -
diagonal_regulartheorem — The diagonal density is continuous and strictly positive throughout the source interval.hypothesesa b :ℝS :ℕhS :0 < Sβ :Fin S → ℝ → ℝ → ℝhcont :∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2) (Set.Icc a b ×ˢ Set.Icc a b)hpos :∀ s x zifx ∈ Set.Icc a bandz ∈ Set.Icc a bthen0 < β s x zconclusionconclusion 1ContinuousOn (diagonalWeight S β) (Set.Icc a b)Proof (Lean source)
theorem diagonal_regular (a b : ℝ) (S : ℕ) (hS : 0 < S) (β : Fin S → ℝ → ℝ → ℝ) (hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2) (Icc a b ×ˢ Icc a b)) (hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z) : ContinuousOn (diagonalWeight S β) (Icc a b) ∧ ∀ x ∈ Icc a b, 0 < diagonalWeight S β x := by -- Compose each coefficient with the diagonal and sum; positivity uses hS. constructor · unfold diagonalWeight apply continuousOn_finsetSum intro s hs have hdiag : ContinuousOn (fun x : ℝ => (x, x)) (Icc a b) := by fun_prop exact (hcont s).comp hdiag (by intro x hx exact ⟨hx, hx⟩) · intro x hx unfold diagonalWeight exact Finset.sum_pos (fun s hs => hpos s x x hx hx) (Finset.univ_nonempty_iff.mpr ⟨⟨0, hS⟩⟩) -
weightedCost_nonnegtheorem — Every feasible paired distortion is nonnegative when its weights are nonnegative on the source square.hypothesesa b :ℝS k :ℕβ :Fin S → ℝ → ℝ → ℝhB :IsMeasurablePartition a b k Bhz :∀ j s, z j s ∈ Icc a bconclusion0 ≤ weightedCost S k β B zProof (Lean source)
theorem weightedCost_nonneg (a b : ℝ) (S k : ℕ) (β : Fin S → ℝ → ℝ → ℝ) (B : Fin k → Set ℝ) (z : Fin k → Fin S → ℝ) (hB : IsMeasurablePartition a b k B) (hz : ∀ j s, z j s ∈ Icc a b) (hβ : ∀ s x y, x ∈ Icc a b → y ∈ Icc a b → 0 ≤ β s x y) : 0 ≤ weightedCost S k β B z := by -- Each cell is contained in Icc a b; integrate pointwise nonnegativity. have hsub (j : Fin k) : B j ⊆ Icc a b := by intro x hx rw [← hB.2.2] exact Set.mem_iUnion.mpr ⟨j, hx⟩ unfold weightedCost apply Finset.sum_nonneg intro j hj apply Finset.sum_nonneg intro s hs apply MeasureTheory.setIntegral_nonneg_ae (hB.1 j) exact Filter.Eventually.of_forall (fun x hx => mul_nonneg (hβ s x (z j s) (hsub j hx) (hz j s)) (abs_nonneg _)) -
optimalCost_le_feasibletheorem — Every feasible code bounds the optimal paired cost from above when the weights are nonnegative on the source square.hypothesesa b :ℝS k :ℕβ :Fin S → ℝ → ℝ → ℝhB :IsMeasurablePartition a b k Bhz :∀ j s, z j s ∈ Icc a bconclusionoptimalCost a b S k β ≤ weightedCost S k β B zProof (Lean source)
theorem optimalCost_le_feasible (a b : ℝ) (S k : ℕ) (β : Fin S → ℝ → ℝ → ℝ) (B : Fin k → Set ℝ) (z : Fin k → Fin S → ℝ) (hB : IsMeasurablePartition a b k B) (hz : ∀ j s, z j s ∈ Icc a b) (hβ : ∀ s x y, x ∈ Icc a b → y ∈ Icc a b → 0 ≤ β s x y) : optimalCost a b S k β ≤ weightedCost S k β B z := by -- weightedCost_nonneg supplies the lower bound needed by csInf_le. apply csInf_le · refine ⟨0, ?_⟩ rintro v ⟨B', z', hB', hz', rfl⟩ exact weightedCost_nonneg a b S k β B' z' hB' hz' hβ · exact ⟨B, z, hB, hz, rfl⟩
LowerBad 2 core · 2 supporting The mass of source points far from at least one reproduction point is controlled by paired distortion, uniformly over arbitrary measurable cells. ★ bad_region_sqrt_mass_cost
The mass of source points far from at least one reproduction point is controlled by paired distortion, uniformly over arbitrary measurable cells.
def badRegion reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Quantization
The bad region of a cell contains points at distance at least δ from one of that cell's reproduction points.
theorem bad_region_sqrt_mass_cost reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Quantization
On a nondegenerate interval from a to b, for a nonempty weight family of continuous positive weights and a measurable partition into k cells with reproduction points in the interval, if every weight is at least a positive constant c on the square and the square root of the diagonal weight is at most a nonnegative constant Q on the interval, and δ is a positive radius, then c·δ times the total square-root diagonal mass of the radius-δ bad regions of all cells is at most Q times the paired weighted cost.
Formal statement
hypotheses
a b :
ℝ
hab :
a < b
S k :
ℕ
hS :
0 < S
β :
Fin S → ℝ → ℝ → ℝ
hcont :
hB :
IsMeasurablePartition a b k B
hz :
∀ j s, z j s ∈ Icc a b
c Q δ :
ℝ
hc :
0 < c
hQ :
0 ≤ Q
hδ :
0 < δ
hupper :
conclusion
≤ Q * weightedCost S k β B z
Proof (Lean source)
theorem bad_region_sqrt_mass_cost (a b : ℝ) (hab : a < b)
(S k : ℕ) (hS : 0 < S)
(β : Fin S → ℝ → ℝ → ℝ)
(hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2)
(Icc a b ×ˢ Icc a b))
(hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z)
(B : Fin k → Set ℝ) (z : Fin k → Fin S → ℝ)
(hB : IsMeasurablePartition a b k B)
(hz : ∀ j s, z j s ∈ Icc a b)
(c Q δ : ℝ) (hc : 0 < c) (hQ : 0 ≤ Q) (hδ : 0 < δ)
(hlower : ∀ s x y, x ∈ Icc a b → y ∈ Icc a b → c ≤ β s x y)
(hupper : ∀ x ∈ Icc a b, sqrt (diagonalWeight S β x) ≤ Q) :
c * δ * (∑ j : Fin k,
∫ x in badRegion S k δ B z j, sqrt (diagonalWeight S β x)) ≤
Q * weightedCost S k β B z := by
-- Apply far_region_measure_cost to each bad region. Integrate the
-- pointwise square-root bound there and sum over cells.
have hsub (j : Fin k) : B j ⊆ Icc a b := by
intro x hx
rw [← hB.2.2]
exact Set.mem_iUnion.mpr ⟨j, hx⟩
have hroot := (sqrt_mass_regular a b hab S hS β hcont hpos).1
have hcell (j : Fin k) :
c * δ * (∫ x in badRegion S k δ B z j,
sqrt (diagonalWeight S β x)) ≤
Q * (∑ s : Fin S, ∫ x in B j, β s x (z j s) * |x - z j s|) := by
let G := badRegion S k δ B z j
have hG : MeasurableSet G := badRegion_measurable S k δ B z hB.1 j
have hGB : G ⊆ B j := fun x hx => hx.1
have hGsub : G ⊆ Icc a b := hGB.trans (hsub j)
have hGfin : volume G ≠ ⊤ :=
(measure_lt_top_of_subset hGsub (measure_Icc_lt_top (μ := volume)).ne).ne
have hInt : IntegrableOn (fun x => sqrt (diagonalWeight S β x)) G volume :=
(hroot.integrableOn_compact isCompact_Icc).mono_set hGsub
have hmass : (∫ x in G, sqrt (diagonalWeight S β x)) ≤
Q * volume.real G := by
calc
(∫ x in G, sqrt (diagonalWeight S β x)) ≤ ∫ _x in G, Q := by
apply setIntegral_mono_on hInt (integrableOn_const hGfin) hG
intro x hx
exact hupper x (hGsub hx)
_ = Q * volume.real G := by
rw [setIntegral_const, smul_eq_mul, mul_comm]
have hIntCost (s : Fin S) : IntegrableOn
(fun x => β s x (z j s) * |x - z j s|) (B j) volume :=
weighted_cell_integrable a b (β s) (hcont s)
(B j) (hsub j) (z j s) (hz j s)
have hcost := far_region_measure_cost a b S β (z j)
(B j) G (hB.1 j) hG (hsub j) hGB c δ hc.le hδ.le
(by intro x hx s; exact hlower s x (z j s) (hGsub hx) (hz j s))
(by intro x hx s; exact (hlower s x (z j s) (hsub j hx) (hz j s)).trans' hc.le)
(by intro x hx; exact hx.2) hIntCost
calc
c * δ * (∫ x in G, sqrt (diagonalWeight S β x)) ≤
c * δ * (Q * volume.real G) :=
mul_le_mul_of_nonneg_left hmass (mul_nonneg hc.le hδ.le)
_ = Q * (c * δ * volume.real G) := by ring
_ ≤ Q * (∑ s : Fin S, ∫ x in B j, β s x (z j s) * |x - z j s|) :=
mul_le_mul_of_nonneg_left hcost hQ
calc
c * δ * (∑ j : Fin k, ∫ x in badRegion S k δ B z j,
sqrt (diagonalWeight S β x)) =
∑ j : Fin k, c * δ * (∫ x in badRegion S k δ B z j,
sqrt (diagonalWeight S β x)) := by rw [Finset.mul_sum]
_ ≤ ∑ j : Fin k, Q * (∑ s : Fin S,
∫ x in B j, β s x (z j s) * |x - z j s|) :=
Finset.sum_le_sum (fun j _ => hcell j)
_ = Q * weightedCost S k β B z := by
simp only [weightedCost, Finset.mul_sum]
2 supporting declarations (lemmas, instances)
-
badRegion_measurabletheorem — The bad region of each measurable cell is measurable, even when the cell is disconnected.hypothesesconclusionMeasurableSet (badRegion S k δ B z j)Proof (Lean source)
theorem badRegion_measurable (S k : ℕ) (δ : ℝ) (B : Fin k → Set ℝ) (z : Fin k → Fin S → ℝ) (hB : ∀ j, MeasurableSet (B j)) : ∀ j, MeasurableSet (badRegion S k δ B z j) := by intro j unfold badRegion measurability -
bad_region_mass_small_of_scaled_cost_boundtheorem — Among candidates whose scaled cost is bounded by a fixed constant, the total square-root mass of points far from at least one reproduction point vanishes uniformly as the number of cells grows.hypothesesconclusion∃ K : ℕ,∀ k : ℕ,K≤ k → 0 < k → ∀ (B : Fin k → Set ℝ) (z : Fin k → Fin S → ℝ), IsMeasurablePartition a b k B → (∀ j s, z j s ∈ Icc a b) → (k : ℝ) * weightedCost S k β B z ≤ M → ∑ j : Fin k, ∫ x in badRegion S k δ B z j, sqrt (diagonalWeight S β x) ≤ εProof (Lean source)
theorem bad_region_mass_small_of_scaled_cost_bound (a b : ℝ) (hab : a < b) (S : ℕ) (hS : 0 < S) (β : Fin S → ℝ → ℝ → ℝ) (hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2) (Icc a b ×ˢ Icc a b)) (hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z) (δ M ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) : ∃ K : ℕ, ∀ k : ℕ, K ≤ k → 0 < k → ∀ (B : Fin k → Set ℝ) (z : Fin k → Fin S → ℝ), IsMeasurablePartition a b k B → (∀ j s, z j s ∈ Icc a b) → (k : ℝ) * weightedCost S k β B z ≤ M → ∑ j : Fin k, ∫ x in badRegion S k δ B z j, sqrt (diagonalWeight S β x) ≤ ε := by -- Compact extrema give c>0 and Q≥0 for bad_region_sqrt_mass_cost. -- Choose K > Q*M/(c*δ*ε), then multiply the distortion bound by k. obtain ⟨c, _C, hc, hcoeff⟩ := coefficient_bounds a b hab S hS β hcont hpos have hroot := (sqrt_mass_regular a b hab S hS β hcont hpos).1 obtain ⟨q, hq, hmax⟩ := isCompact_Icc.exists_isMaxOn (s := Icc a b) ⟨a, le_refl a, hab.le⟩ hroot let Q : ℝ := sqrt (diagonalWeight S β q) have hQ : 0 ≤ Q := Real.sqrt_nonneg _ have hupper : ∀ x ∈ Icc a b, sqrt (diagonalWeight S β x) ≤ Q := by intro x hx exact hmax hx have hden : 0 < c * δ * ε := mul_pos (mul_pos hc hδ) hε obtain ⟨K, hK⟩ := exists_nat_gt (Q * M / (c * δ * ε)) refine ⟨K, ?_⟩ intro k hkK hk B z hB hz hcost let bad : ℝ := ∑ j : Fin k, ∫ x in badRegion S k δ B z j, sqrt (diagonalWeight S β x) have hbad : c * δ * bad ≤ Q * weightedCost S k β B z := by exact bad_region_sqrt_mass_cost a b hab S k hS β hcont hpos B z hB hz c Q δ hc hQ hδ (by intro s x y hx hy; exact (hcoeff s x hx y hy).1) hupper have hmul : (k : ℝ) * (c * δ * bad) ≤ Q * M := by calc (k : ℝ) * (c * δ * bad) ≤ (k : ℝ) * (Q * weightedCost S k β B z) := mul_le_mul_of_nonneg_left hbad (Nat.cast_nonneg k) _ = Q * ((k : ℝ) * weightedCost S k β B z) := by ring _ ≤ Q * M := mul_le_mul_of_nonneg_left hcost hQ have hkR : (K : ℝ) ≤ (k : ℝ) := by exact_mod_cast hkK have hthreshold : Q * M < (k : ℝ) * (c * δ * ε) := by exact (div_lt_iff₀ hden).mp (lt_of_lt_of_le hK hkR) by_contra hnot have hgt : ε < bad := lt_of_not_ge hnot have hkd : 0 < (k : ℝ) * (c * δ) := mul_pos (Nat.cast_pos.mpr hk) (mul_pos hc hδ) have hstrict : (k : ℝ) * (c * δ * ε) < (k : ℝ) * (c * δ * bad) := by nlinarith [mul_lt_mul_of_pos_left hgt hkd] linarith
Companding 5 core · 7 supporting Equal-square-root-mass companding boundaries, ordered cells, midpoint reproduction, and uniform continuity estimates on fine cells. ★ companding_feasible
Equal-square-root-mass companding boundaries, ordered cells, midpoint reproduction, and uniform continuity estimates on fine cells.
def boundary reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Quantization
The jth companding boundary is the first source point at which cumulative square-root-diagonal mass reaches the fraction j/k of total mass.
Definition (Lean source)
parameters
def
boundary a b S k j β :
ℝ
given by
sInf {x : ℝ | x ∈ Icc a b ∧ (j : ℝ) / k * (∫ t in a..b, sqrt (diagonalWeight S β t)) ≤ ∫ t in a..x, sqrt (diagonalWeight S β t)}
def compandingCell reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Quantization
The jth ordered companding cell is half-open except at the final right endpoint, where it is closed.
def compandingMidpoint reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Quantization
Every coefficient in a companding cell uses the same interval midpoint as its reproduction point.
theorem companding_feasible reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Quantization
On a nondegenerate interval from a to b, for a nonempty family of jointly continuous strictly positive weights and a positive number of cells, the companding cells form a measurable partition of the interval, and every cell midpoint lies in the interval.
Formal statement
hypotheses
conclusion
conclusion 1
IsMeasurablePartition a b k (compandingCell a b S k β)
Proof (Lean source)
theorem companding_feasible (a b : ℝ) (hab : a < b)
(S k : ℕ) (hS : 0 < S) (hk : 0 < k)
(β : Fin S → ℝ → ℝ → ℝ)
(hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2)
(Icc a b ×ˢ Icc a b))
(hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z) :
IsMeasurablePartition a b k (compandingCell a b S k β) ∧
∀ j s, compandingMidpoint a b S k β j s ∈ Icc a b := by
classical
obtain ⟨hfirst, hlast, hstrict⟩ :=
boundary_order a b hab S k hS hk β hcont hpos
let A : ℕ → ℝ := fun n => boundary a b S k n β
have hmem (n : ℕ) (hn : n ≤ k) : A n ∈ Icc a b :=
(boundary_equal_mass a b hab S k n hS hk hn β hcont hpos).1
have hcell_bounds (j : Fin k) (x : ℝ)
(hx : x ∈ compandingCell a b S k β j) :
A j.val ≤ x ∧ x ≤ A (j.val + 1) := by
unfold compandingCell at hx
split_ifs at hx with h
· exact hx
· exact ⟨hx.1, hx.2.le⟩
have hcell_open (j : Fin k) (hj : j.val + 1 < k) (x : ℝ)
(hx : x ∈ compandingCell a b S k β j) : x < A (j.val + 1) := by
unfold compandingCell at hx
split_ifs at hx with h
· omega
· exact hx.2
have hmeas (j : Fin k) : MeasurableSet (compandingCell a b S k β j) := by
unfold compandingCell
split_ifs <;> measurability
have hdisj : ∀ i j : Fin k, i ≠ j →
Disjoint (compandingCell a b S k β i)
(compandingCell a b S k β j) := by
intro i j hne
apply Set.disjoint_left.mpr
intro x hxi hxj
have hi : i.val < j.val ∨ j.val < i.val :=
lt_or_gt_of_ne (Fin.val_injective.ne hne)
rcases hi with hij | hji
· have hnext : i.val + 1 ≤ j.val := by omega
have hupper : A (i.val + 1) ≤ A j.val := by
rcases eq_or_lt_of_le hnext with heq | hlt
· exact le_of_eq (congrArg A heq)
· exact (hstrict _ _ hlt j.isLt.le).le
have hxi' := hcell_open i (by omega) x hxi
have hxj' := (hcell_bounds j x hxj).1
linarith
· have hnext : j.val + 1 ≤ i.val := by omega
have hupper : A (j.val + 1) ≤ A i.val := by
rcases eq_or_lt_of_le hnext with heq | hlt
· exact le_of_eq (congrArg A heq)
· exact (hstrict _ _ hlt i.isLt.le).le
have hxj' := hcell_open j (by omega) x hxj
have hxi' := (hcell_bounds i x hxi).1
linarith
have hcover : (⋃ j : Fin k, compandingCell a b S k β j) =
Icc a b := by
ext x
constructor
· intro hx
obtain ⟨j, hj⟩ := Set.mem_iUnion.mp hx
obtain ⟨hl, hu⟩ := hcell_bounds j x hj
exact ⟨(hmem j.val j.isLt.le).1.trans hl,
hu.trans (hmem (j.val + 1) (by omega)).2⟩
· intro hx
by_cases hxb : x = b
· let j : Fin k := ⟨k - 1, by omega⟩
have hjlast : j.val + 1 = k := by dsimp [j]; omega
apply Set.mem_iUnion.mpr
refine ⟨j, ?_⟩
unfold compandingCell
rw [if_pos hjlast]
rw [hjlast, hlast]
subst x
exact ⟨(hmem j.val j.isLt.le).2, le_refl b⟩
· have hxab : x ∈ Ico (A 0) (A k) := by
simpa [A, hfirst, hlast] using (show x ∈ Ico a b from ⟨hx.1, lt_of_le_of_ne hx.2 hxb⟩)
have hxunion := Ico_subset_biUnion_Ico k A hxab
simp only [Set.mem_iUnion, Finset.mem_range] at hxunion
obtain ⟨n, hn, hxn⟩ := hxunion
let j : Fin k := ⟨n, hn⟩
apply Set.mem_iUnion.mpr
refine ⟨j, ?_⟩
unfold compandingCell
by_cases hlastj : j.val + 1 = k
· rw [if_pos hlastj]
exact ⟨hxn.1, hxn.2.le⟩
· rw [if_neg hlastj]
exact hxn
refine ⟨⟨hmeas, hdisj, hcover⟩, ?_⟩
intro j s
unfold compandingMidpoint
have hj0 := hmem j.val j.isLt.le
have hj1 := hmem (j.val + 1) (by omega)
exact ⟨by linarith [hj0.1, hj1.1], by linarith [hj0.2, hj1.2]⟩
def compandingSurrogateCost reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Quantization
The midpoint diagonal-weight surrogate cost of the k-cell companding partition is the sum over cells of the diagonal weight at the cell midpoint times the squared cell length divided by four. It is what the paired cost becomes when each cell's varying weights are replaced by their diagonal value at its midpoint.
7 supporting declarations (lemmas, instances)
-
boundary_equal_masstheorem — Every valid companding boundary divides cumulative square-root-diagonal mass at precisely its prescribed fraction.hypothesesconclusionconclusion 2(∫ t in a..boundary a b S k j β, sqrt (diagonalWeight S β t))= (j : ℝ) / k * (∫ t in a..b, sqrt (diagonalWeight S β t))Proof (Lean source)
theorem boundary_equal_mass (a b : ℝ) (hab : a < b) (S k j : ℕ) (hS : 0 < S) (hk : 0 < k) (hj : j ≤ k) (β : Fin S → ℝ → ℝ → ℝ) (hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2) (Icc a b ×ˢ Icc a b)) (hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z) : boundary a b S k j β ∈ Icc a b ∧ (∫ t in a..boundary a b S k j β, sqrt (diagonalWeight S β t)) = (j : ℝ) / k * (∫ t in a..b, sqrt (diagonalWeight S β t)) := by let f : ℝ → ℝ := fun x => sqrt (diagonalWeight S β x) let F : ℝ → ℝ := fun x => ∫ t in a..x, f t have hf : ContinuousOn f (Icc a b) := (sqrt_mass_regular a b hab S hS β hcont hpos).1 have hfpos : ∀ x ∈ Icc a b, 0 < f x := by intro x hx exact Real.sqrt_pos.2 ((diagonal_regular a b S hS β hcont hpos).2 x hx) have hFcont : ContinuousOn F (Icc a b) := by have hfi : IntegrableOn f (Icc a b) := hf.integrableOn_Icc have hfu : IntegrableOn f (uIcc a b) := by simpa only [Set.uIcc_of_le hab.le] using hfi have hc : ContinuousOn F (uIcc a b) := intervalIntegral.continuousOn_primitive_interval (a := a) (b := b) hfu simpa only [Set.uIcc_of_le hab.le] using hc have hFstrict : ∀ x ∈ Icc a b, ∀ y ∈ Icc a b, x < y → F x < F y := by intro x hx y hy hxy have hxycont : ContinuousOn f (Icc x y) := hf.mono (by intro z hz; exact ⟨hx.1.trans hz.1, hz.2.trans hy.2⟩) have hpositive : 0 < ∫ t in x..y, f t := intervalIntegral.integral_pos hxy hxycont (by intro z hz; exact (hfpos z ⟨hx.1.trans (le_of_lt hz.1), hz.2.trans hy.2⟩).le) ⟨x, ⟨le_refl x, hxy.le⟩, hfpos x hx⟩ have hax : IntervalIntegrable f volume a x := ContinuousOn.intervalIntegrable_of_Icc hx.1 (hf.mono (by intro z hz; exact ⟨hz.1, hz.2.trans hx.2⟩)) have hxyint : IntervalIntegrable f volume x y := ContinuousOn.intervalIntegrable_of_Icc hxy.le hxycont have hadd := intervalIntegral.integral_add_adjacent_intervals hax hxyint dsimp [F] linarith have hmass : 0 < F b := (sqrt_mass_regular a b hab S hS β hcont hpos).2 have hFzero : F a = 0 := by simp [F] have htarget : F a ≤ (j : ℝ) / k * F b ∧ (j : ℝ) / k * F b ≤ F b := by rw [hFzero] have hkreal : (0 : ℝ) < k := by exact_mod_cast hk have hjreal : (j : ℝ) ≤ k := by exact_mod_cast hj constructor · exact mul_nonneg (div_nonneg (Nat.cast_nonneg _) hkreal.le) hmass.le · exact mul_le_of_le_one_left hmass.le (div_le_one_of_le₀ hjreal hkreal.le) obtain ⟨x, hx, hFx'⟩ := intermediate_value_Icc hab.le hFcont htarget have hxset : x ∈ {y : ℝ | y ∈ Icc a b ∧ (j : ℝ) / k * F b ≤ F y} := ⟨hx, hFx'.ge⟩ have hleast : ∀ y ∈ {y : ℝ | y ∈ Icc a b ∧ (j : ℝ) / k * F b ≤ F y}, x ≤ y := by intro y hy by_contra h have hyx : y < x := lt_of_not_ge h exact (not_lt_of_ge hy.2) (hFx' ▸ hFstrict y hy.1 x hx hyx) have hboundary : boundary a b S k j β = x := by unfold boundary apply le_antisymm · exact csInf_le ⟨a, by rintro y ⟨hy, _⟩; exact hy.1⟩ hxset · exact le_csInf ⟨x, hxset⟩ hleast rw [hboundary] exact ⟨hx, hFx'⟩ -
boundary_ordertheorem — Companding boundaries start at the left endpoint, end at the right endpoint, and strictly increase with their valid indices.hypothesesProof (Lean source)
theorem boundary_order (a b : ℝ) (hab : a < b) (S k : ℕ) (hS : 0 < S) (hk : 0 < k) (β : Fin S → ℝ → ℝ → ℝ) (hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2) (Icc a b ×ˢ Icc a b)) (hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z) : boundary a b S k 0 β = a ∧ boundary a b S k k β = b ∧ ∀ i j, i < j → j ≤ k → boundary a b S k i β < boundary a b S k j β := by let f : ℝ → ℝ := fun x => sqrt (diagonalWeight S β x) let F : ℝ → ℝ := fun x => ∫ t in a..x, f t have hf : ContinuousOn f (Icc a b) := (sqrt_mass_regular a b hab S hS β hcont hpos).1 have hfpos : ∀ x ∈ Icc a b, 0 < f x := by intro x hx exact Real.sqrt_pos.2 ((diagonal_regular a b S hS β hcont hpos).2 x hx) have hFstrict : ∀ x ∈ Icc a b, ∀ y ∈ Icc a b, x < y → F x < F y := by intro x hx y hy hxy have hxycont : ContinuousOn f (Icc x y) := hf.mono (by intro z hz; exact ⟨hx.1.trans hz.1, hz.2.trans hy.2⟩) have hpositive : 0 < ∫ t in x..y, f t := intervalIntegral.integral_pos hxy hxycont (by intro z hz; exact (hfpos z ⟨hx.1.trans (le_of_lt hz.1), hz.2.trans hy.2⟩).le) ⟨x, ⟨le_refl x, hxy.le⟩, hfpos x hx⟩ have hax : IntervalIntegrable f volume a x := ContinuousOn.intervalIntegrable_of_Icc hx.1 (hf.mono (by intro z hz; exact ⟨hz.1, hz.2.trans hx.2⟩)) have hxyint : IntervalIntegrable f volume x y := ContinuousOn.intervalIntegrable_of_Icc hxy.le hxycont have hadd := intervalIntegral.integral_add_adjacent_intervals hax hxyint dsimp [F] linarith have hbound (j : ℕ) (hj : j ≤ k) : boundary a b S k j β ∈ Icc a b ∧ F (boundary a b S k j β) = (j : ℝ) / k * F b := boundary_equal_mass a b hab S k j hS hk hj β hcont hpos have hzero : boundary a b S k 0 β = a := by obtain ⟨hx, heq⟩ := hbound 0 (zero_le k) by_contra h have hlt : a < boundary a b S k 0 β := lt_of_le_of_ne hx.1 (Ne.symm h) have hstrict := hFstrict a ⟨le_refl a, hab.le⟩ _ hx hlt simp [F] at heq hstrict linarith have hlast : boundary a b S k k β = b := by obtain ⟨hx, heq⟩ := hbound k (le_refl k) by_contra h have hlt : boundary a b S k k β < b := lt_of_le_of_ne hx.2 h have hstrict := hFstrict _ hx b ⟨hab.le, le_refl b⟩ hlt have hkreal : (k : ℝ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hk) simp [hkreal] at heq linarith refine ⟨hzero, hlast, ?_⟩ intro i j hij hj obtain ⟨hi_mem, hi_eq⟩ := hbound i (le_trans (le_of_lt hij) hj) obtain ⟨hj_mem, hj_eq⟩ := hbound j hj by_contra h have hji : boundary a b S k j β ≤ boundary a b S k i β := le_of_not_gt h have hFji : F (boundary a b S k j β) ≤ F (boundary a b S k i β) := by rcases hji.eq_or_lt with heq | hlt · rw [heq] · exact (hFstrict _ hj_mem _ hi_mem hlt).le have hmass : 0 < F b := (sqrt_mass_regular a b hab S hS β hcont hpos).2 have hkreal : (0 : ℝ) < k := by exact_mod_cast hk have hijreal : (i : ℝ) < j := by exact_mod_cast hij rw [hi_eq, hj_eq] at hFji have hfrac : (i : ℝ) / k < (j : ℝ) / k := (div_lt_div_iff_of_pos_right hkreal).2 (by nlinarith) nlinarith -
companding_interval_masstheorem — Each companding cell has exactly one kth of the total square-root diagonal mass, expressed as an integral between its consecutive boundaries.hypothesesconclusion= (∫ x in a..b, sqrt (diagonalWeight S β x)) / kProof (Lean source)
theorem companding_interval_mass (a b : ℝ) (hab : a < b) (S k : ℕ) (hS : 0 < S) (hk : 0 < k) (β : Fin S → ℝ → ℝ → ℝ) (hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2) (Icc a b ×ˢ Icc a b)) (hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z) (j : Fin k) : (∫ x in boundary a b S k j.val β..boundary a b S k (j.val + 1) β, sqrt (diagonalWeight S β x)) = (∫ x in a..b, sqrt (diagonalWeight S β x)) / k := by -- Subtract the two boundary_equal_mass identities using integral_add_adjacent_intervals. have h0 := boundary_equal_mass a b hab S k j.val hS hk j.isLt.le β hcont hpos have h1 := boundary_equal_mass a b hab S k (j.val + 1) hS hk (by omega) β hcont hpos have hf := (sqrt_mass_regular a b hab S hS β hcont hpos).1 have hi0 : IntervalIntegrable (fun x => sqrt (diagonalWeight S β x)) volume a (boundary a b S k j.val β) := ContinuousOn.intervalIntegrable_of_Icc h0.1.1 (hf.mono (by intro x hx; exact ⟨hx.1, hx.2.trans h0.1.2⟩)) have hi1 : IntervalIntegrable (fun x => sqrt (diagonalWeight S β x)) volume (boundary a b S k j.val β) (boundary a b S k (j.val + 1) β) := by have hord := (boundary_order a b hab S k hS hk β hcont hpos).2.2 j.val (j.val + 1) (by omega) (by omega) exact ContinuousOn.intervalIntegrable_of_Icc hord.le (hf.mono (by intro x hx; exact ⟨h0.1.1.trans hx.1, hx.2.trans h1.1.2⟩)) have hadd := intervalIntegral.integral_add_adjacent_intervals hi0 hi1 rw [h0.2, h1.2] at hadd have hkreal : (k : ℝ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hk) have hcast : ((j.val + 1 : ℕ) : ℝ) = (j.val : ℝ) + 1 := by norm_cast rw [hcast] at hadd calc (∫ x in boundary a b S k j.val β..boundary a b S k (j.val + 1) β, sqrt (diagonalWeight S β x)) = ((j.val : ℝ) + 1) / k * (∫ x in a..b, sqrt (diagonalWeight S β x)) - (j.val : ℝ) / k * (∫ x in a..b, sqrt (diagonalWeight S β x)) := by linarith [hadd] _ = (∫ x in a..b, sqrt (diagonalWeight S β x)) / k := by ring -
companding_length_boundtheorem — A positive uniform lower bound for square-root diagonal mass forces every companding cell length to be at most a constant times 1/k.hypothesesProof (Lean source)
theorem companding_length_bound (a b : ℝ) (hab : a < b) (S : ℕ) (hS : 0 < S) (β : Fin S → ℝ → ℝ → ℝ) (hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2) (Icc a b ×ˢ Icc a b)) (hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z) : ∃ c : ℝ, 0 < c ∧ ∀ k : ℕ, 0 < k → ∀ j : Fin k, c * (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) ≤ (∫ x in a..b, sqrt (diagonalWeight S β x)) / k := by -- Minimize the positive continuous square-root weight on Icc a b, then -- compare its constant lower bound with companding_interval_mass. let f : ℝ → ℝ := fun x => sqrt (diagonalWeight S β x) have hf := (sqrt_mass_regular a b hab S hS β hcont hpos).1 obtain ⟨c, hc, hcf⟩ := isCompact_Icc.exists_forall_le' hf (a := (0 : ℝ)) (by intro x hx exact Real.sqrt_pos.2 ((diagonal_regular a b S hS β hcont hpos).2 x hx)) refine ⟨c, hc, ?_⟩ intro k hk j have h0 := (boundary_equal_mass a b hab S k j.val hS hk j.isLt.le β hcont hpos).1 have h1 := (boundary_equal_mass a b hab S k (j.val + 1) hS hk (by omega) β hcont hpos).1 have hord := (boundary_order a b hab S k hS hk β hcont hpos).2.2 j.val (j.val + 1) (by omega) (by omega) have hfi : IntervalIntegrable f volume (boundary a b S k j.val β) (boundary a b S k (j.val + 1) β) := ContinuousOn.intervalIntegrable_of_Icc hord.le (hf.mono (by intro x hx; exact ⟨h0.1.trans hx.1, hx.2.trans h1.2⟩)) have hmono := intervalIntegral.integral_mono_on hord.le intervalIntegrable_const hfi (by intro x hx; exact hcf x ⟨h0.1.trans hx.1, hx.2.trans h1.2⟩) rw [intervalIntegral.integral_const] at hmono simpa only [smul_eq_mul, mul_comm] using (hmono.trans_eq (companding_interval_mass a b hab S k hS hk β hcont hpos j)) -
companding_cell_midpoint_momenttheorem — The absolute-distance integral over each half-open companding cell is exactly one quarter of the square of its endpoint separation.hypothesesconclusion(∫ x in compandingCell a b S k β j, |x - compandingMidpoint a b S k β j s|)Proof (Lean source)
theorem companding_cell_midpoint_moment (a b : ℝ) (hab : a < b) (S k : ℕ) (hS : 0 < S) (hk : 0 < k) (β : Fin S → ℝ → ℝ → ℝ) (hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2) (Icc a b ×ˢ Icc a b)) (hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z) (j : Fin k) (s : Fin S) : (∫ x in compandingCell a b S k β j, |x - compandingMidpoint a b S k β j s|) = (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) ^ 2 / 4 := by have hord := (boundary_order a b hab S k hS hk β hcont hpos).2.2 j.val (j.val + 1) (by omega) (by omega) unfold compandingCell compandingMidpoint split_ifs with hlast · rw [integral_Icc_eq_integral_Ioc, ← intervalIntegral.integral_of_le hord.le] exact interval_midpoint_moment _ _ hord.le · rw [integral_Ico_eq_integral_Ioc, ← intervalIntegral.integral_of_le hord.le] exact interval_midpoint_moment _ _ hord.le -
companding_midpoint_mass_error_eventuallytheorem — On sufficiently fine companding cells, the midpoint square-root weight times cell length differs from the cell's exact equal mass by at most an arbitrarily small multiple of that length, uniformly across cells.hypothesesconclusion∃ K : ℕ,∀ k : ℕ,K≤ k → 0 < k → ∀ j : Fin k, |sqrt (diagonalWeight S β ((boundary a b S k j.val β + boundary a b S k (j.val + 1) β) / 2)) * (boundary a b S k (j.val + 1) β - boundary a b S k j.val β)- (∫ x in a..b, sqrt (diagonalWeight S β x)) / k|Proof (Lean source)
theorem companding_midpoint_mass_error_eventually (a b : ℝ) (hab : a < b) (S : ℕ) (hS : 0 < S) (β : Fin S → ℝ → ℝ → ℝ) (hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2) (Icc a b ×ˢ Icc a b)) (hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z) : ∀ η : ℝ, 0 < η → ∃ K : ℕ, ∀ k : ℕ, K ≤ k → 0 < k → ∀ j : Fin k, |sqrt (diagonalWeight S β ((boundary a b S k j.val β + boundary a b S k (j.val + 1) β) / 2)) * (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) - (∫ x in a..b, sqrt (diagonalWeight S β x)) / k| ≤ η * (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) := by -- Use uniform continuity of sqrt(diagonalWeight) on Icc a b and -- companding_length_bound to make every cell shorter than its modulus. -- Integrate the pointwise midpoint error, then use companding_interval_mass. intro η hη let f : ℝ → ℝ := fun x => sqrt (diagonalWeight S β x) have hf : ContinuousOn f (Icc a b) := (sqrt_mass_regular a b hab S hS β hcont hpos).1 have hu := isCompact_Icc.uniformContinuousOn_of_continuous hf obtain ⟨δ, hδ, huc⟩ := (Metric.uniformContinuousOn_iff.mp hu) η hη obtain ⟨c, hc, hbound⟩ := companding_length_bound a b hab S hS β hcont hpos let M : ℝ := ∫ x in a..b, f x obtain ⟨K, hK⟩ := exists_nat_gt (M / (c * δ)) refine ⟨K, ?_⟩ intro k hkK hk j let l := boundary a b S k j.val β let r := boundary a b S k (j.val + 1) β let m := (l + r) / 2 have hl : l ∈ Icc a b := (boundary_equal_mass a b hab S k j.val hS hk j.isLt.le β hcont hpos).1 have hr : r ∈ Icc a b := (boundary_equal_mass a b hab S k (j.val + 1) hS hk (by omega) β hcont hpos).1 have hord : l ≤ r := ((boundary_order a b hab S k hS hk β hcont hpos).2.2 j.val (j.val + 1) (by omega) (by omega)).le have hm : m ∈ Icc a b := ⟨by dsimp [m]; linarith [hl.1, hr.1], by dsimp [m]; linarith [hl.2, hr.2]⟩ have hkreal : (0 : ℝ) < k := by exact_mod_cast hk have hKreal : (K : ℝ) ≤ k := by exact_mod_cast hkK have hshort : r - l < δ := by have hlen := hbound k hk j have hmass : M < (k : ℝ) * (c * δ) := (div_lt_iff₀ (mul_pos hc hδ)).mp (lt_of_lt_of_le hK hKreal) have hlen' : c * (r - l) * (k : ℝ) ≤ M := (le_div_iff₀ hkreal).mp hlen by_contra hn have hge := mul_le_mul_of_nonneg_left (le_of_not_gt hn) hc.le have hge' := mul_le_mul_of_nonneg_left hge hkreal.le nlinarith have hfi : IntervalIntegrable f volume l r := ContinuousOn.intervalIntegrable_of_Icc hord (hf.mono (by intro x hx; exact ⟨hl.1.trans hx.1, hx.2.trans hr.2⟩)) have hpoint : ∀ x ∈ Set.uIoc l r, ‖f m - f x‖ ≤ η := by intro x hx rw [Set.uIoc_of_le hord] at hx have hxmem : x ∈ Icc a b := ⟨hl.1.trans hx.1.le, hx.2.trans hr.2⟩ have hmx : |m - x| ≤ r - l := by apply abs_le.mpr dsimp [m] constructor <;> linarith [hx.1, hx.2] have hdist : dist m x < δ := by simpa [Real.dist_eq] using (lt_of_le_of_lt hmx hshort) simpa [Real.norm_eq_abs, Real.dist_eq] using (huc m hm x hxmem hdist).le have hnorm := intervalIntegral.norm_integral_le_of_norm_le_const hpoint have heq : f m * (r - l) - M / k = ∫ x in l..r, (f m - f x) := by rw [← companding_interval_mass a b hab S k hS hk β hcont hpos j] rw [intervalIntegral.integral_sub intervalIntegrable_const hfi, intervalIntegral.integral_const] simp only [smul_eq_mul] ring rw [show sqrt (diagonalWeight S β ((boundary a b S k j.val β + boundary a b S k (j.val + 1) β) / 2)) = f m from rfl] change |f m * (r - l) - M / k| ≤ η * (r - l) rw [heq, ← Real.norm_eq_abs] simpa only [abs_of_nonneg (sub_nonneg.mpr hord)] using hnorm -
companding_coefficient_error_eventuallytheorem — On sufficiently fine companding cells, each actual coefficient differs from its midpoint diagonal value by at most any prescribed positive error.hypothesesconclusion∃ K : ℕ,∀ k : ℕ,K≤ k → 0 < k → ∀ (j : Fin k) (s : Fin S) (x : ℝ), x ∈ compandingCell a b S k β j → |β s x (compandingMidpoint a b S k β j s)- β s (compandingMidpoint a b S k β j s) (compandingMidpoint a b S k β j s)| ≤ ηProof (Lean source)
theorem companding_coefficient_error_eventually (a b : ℝ) (hab : a < b) (S : ℕ) (hS : 0 < S) (β : Fin S → ℝ → ℝ → ℝ) (hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2) (Icc a b ×ˢ Icc a b)) (hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z) : ∀ η : ℝ, 0 < η → ∃ K : ℕ, ∀ k : ℕ, K ≤ k → 0 < k → ∀ (j : Fin k) (s : Fin S) (x : ℝ), x ∈ compandingCell a b S k β j → |β s x (compandingMidpoint a b S k β j s) - β s (compandingMidpoint a b S k β j s) (compandingMidpoint a b S k β j s)| ≤ η := by -- Uniform continuity on the compact square controls the pairs (x,m) -- and (m,m); companding_length_bound makes their distance uniformly small. intro η hη obtain ⟨δ, hδ, huc⟩ := coefficient_uniform_continuity a b S β hcont η hη obtain ⟨c, hc, hbound⟩ := companding_length_bound a b hab S hS β hcont hpos let M : ℝ := ∫ x in a..b, sqrt (diagonalWeight S β x) obtain ⟨K, hK⟩ := exists_nat_gt (M / (c * δ)) refine ⟨K, ?_⟩ intro k hkK hk j s x hx let l := boundary a b S k j.val β let r := boundary a b S k (j.val + 1) β let m := compandingMidpoint a b S k β j s have hl : l ∈ Icc a b := (boundary_equal_mass a b hab S k j.val hS hk j.isLt.le β hcont hpos).1 have hr : r ∈ Icc a b := (boundary_equal_mass a b hab S k (j.val + 1) hS hk (by omega) β hcont hpos).1 have hm : m ∈ Icc a b := (companding_feasible a b hab S k hS hk β hcont hpos).2 j s have hxr : l ≤ x ∧ x ≤ r := by unfold compandingCell at hx split_ifs at hx with h · exact hx · exact ⟨hx.1, hx.2.le⟩ have hxmem : x ∈ Icc a b := ⟨hl.1.trans hxr.1, hxr.2.trans hr.2⟩ have hkreal : (0 : ℝ) < k := by exact_mod_cast hk have hKreal : (K : ℝ) ≤ k := by exact_mod_cast hkK have hshort : r - l < δ := by have hlen := hbound k hk j have hmass : M < (k : ℝ) * (c * δ) := (div_lt_iff₀ (mul_pos hc hδ)).mp (lt_of_lt_of_le hK hKreal) have hlen' : c * (r - l) * (k : ℝ) ≤ M := (le_div_iff₀ hkreal).mp hlen by_contra hn have hge := mul_le_mul_of_nonneg_left (le_of_not_gt hn) hc.le have hge' := mul_le_mul_of_nonneg_left hge hkreal.le nlinarith have hxm : |x - m| ≤ r - l := by dsimp [m, compandingMidpoint] apply abs_le.mpr constructor <;> dsimp [l, r] at * <;> linarith have hdist : dist (x, m) (m, m) < δ := by simpa [dist_prod_same_right, Real.dist_eq] using (lt_of_le_of_lt hxm hshort) exact (huc s (x, m) (m, m) ⟨hxmem, hm⟩ ⟨hm, hm⟩ hdist).le
CompandingLimits 1 core · 5 supporting Finite mesh estimates and exact scaled limits for equal-mass companding cells. ★ companding_scaled_cost_tendsto
Finite mesh estimates and exact scaled limits for equal-mass companding cells. The estimates isolate the analytic and algebraic steps of the limit.
theorem companding_scaled_cost_tendsto reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Quantization
On a nondegenerate interval from a to b, for a nonempty finite weight family that is jointly continuous and strictly positive on the square, k times the paired weighted cost of the k-cell companding partition with midpoint reproduction points converges, as k tends to infinity, to one quarter of the square of the integral over the interval of the square root of the diagonal weight.
Formal statement
hypotheses
conclusion
Tendsto (fun k : ℕ => (k : ℝ) * weightedCost S k β (compandingCell a b S k β) (compandingMidpoint a b S k β)) atTop (nhds ((1 / 4 : ℝ) * (∫ x in a..b, sqrt (diagonalWeight S β x)) ^ 2))
Proof (Lean source)
theorem companding_scaled_cost_tendsto (a b : ℝ) (hab : a < b)
(S : ℕ) (hS : 0 < S) (β : Fin S → ℝ → ℝ → ℝ)
(hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2)
(Icc a b ×ˢ Icc a b))
(hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z) :
Tendsto (fun k : ℕ => (k : ℝ) * weightedCost S k β
(compandingCell a b S k β) (compandingMidpoint a b S k β))
atTop (nhds ((1 / 4 : ℝ) *
(∫ x in a..b, sqrt (diagonalWeight S β x)) ^ 2)) := by
have hsurrogate := companding_surrogate_scaled_tendsto a b hab S hS β hcont hpos
have herr := companding_surrogate_error_tendsto a b hab S hS β hcont hpos
convert hsurrogate.add herr using 1
· ext k
ring
· simp
5 supporting declarations (lemmas, instances)
-
companding_scaled_length_square_boundtheorem — The scaled sum of squared companding cell lengths is uniformly bounded over every positive cell count. This follows from the equal-mass length bound and the telescoping sum of cell lengths.hypothesesProof (Lean source)
theorem companding_scaled_length_square_bound (a b : ℝ) (hab : a < b) (S : ℕ) (hS : 0 < S) (β : Fin S → ℝ → ℝ → ℝ) (hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2) (Icc a b ×ˢ Icc a b)) (hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z) : ∃ C : ℝ, 0 < C ∧ ∀ k : ℕ, 0 < k → (k : ℝ) * ∑ j : Fin k, (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) ^ 2 ≤ C := by classical obtain ⟨c, hc, hlen⟩ := companding_length_bound a b hab S hS β hcont hpos let M : ℝ := ∫ x in a..b, sqrt (diagonalWeight S β x) refine ⟨M / c * (b - a) + 1, ?_, ?_⟩ · have hM : 0 < M := (sqrt_mass_regular a b hab S hS β hcont hpos).2 positivity intro k hk have hkreal : (0 : ℝ) < k := by exact_mod_cast hk have hord := (boundary_order a b hab S k hS hk β hcont hpos).2.2 have hcell (j : Fin k) : (k : ℝ) * (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) ^ 2 ≤ (M / c) * (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) := by have hp : 0 ≤ boundary a b S k (j.val + 1) β - boundary a b S k j.val β := sub_nonneg.mpr ((hord j.val (j.val + 1) (by omega) (by omega)).le) have hb := hlen k hk j have hh : (k : ℝ) * (c * (boundary a b S k (j.val + 1) β - boundary a b S k j.val β)) ≤ M := by calc _ = c * (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) * k := by ring _ ≤ M := (le_div_iff₀ hkreal).mp hb have hprod := mul_le_mul_of_nonneg_right hh hp calc _ ≤ M * (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) / c := (le_div_iff₀ hc).2 (by nlinarith [hprod]) _ = _ := by ring have hsum := Finset.sum_le_sum (s := univ) (fun j _ => hcell j) have htel : (∑ j : Fin k, (boundary a b S k (j.val + 1) β - boundary a b S k j.val β)) = b - a := by calc _ = boundary a b S k k β - boundary a b S k 0 β := by simpa only [Finset.sum_range] using (Finset.sum_range_sub (fun n => boundary a b S k n β) k) _ = b - a := by obtain ⟨hfirst, hlast, _⟩ := boundary_order a b hab S k hS hk β hcont hpos rw [hfirst, hlast] rw [← Finset.mul_sum, ← Finset.mul_sum, htel] at hsum linarith -
companding_surrogate_cell_error_eventuallytheorem — The squared midpoint mass of each sufficiently fine companding cell differs from the square of its exact equal mass by at most a prescribed multiple of the squared cell length.hypothesesconclusion∃ K : ℕ,∀ k : ℕ,K≤ k → 0 < k → ∀ j : Fin k, |diagonalWeight S β ((boundary a b S k j.val β + boundary a b S k (j.val + 1) β) / 2) * (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) ^ 2- ((∫ x in a..b, sqrt (diagonalWeight S β x)) / k) ^ 2|Proof (Lean source)
theorem companding_surrogate_cell_error_eventually (a b : ℝ) (hab : a < b) (S : ℕ) (hS : 0 < S) (β : Fin S → ℝ → ℝ → ℝ) (hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2) (Icc a b ×ˢ Icc a b)) (hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z) : ∀ η : ℝ, 0 < η → ∃ K : ℕ, ∀ k : ℕ, K ≤ k → 0 < k → ∀ j : Fin k, |diagonalWeight S β ((boundary a b S k j.val β + boundary a b S k (j.val + 1) β) / 2) * (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) ^ 2 - ((∫ x in a..b, sqrt (diagonalWeight S β x)) / k) ^ 2| ≤ η * (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) ^ 2 := by intro η hη let f : ℝ → ℝ := fun x => sqrt (diagonalWeight S β x) have hf := (sqrt_mass_regular a b hab S hS β hcont hpos).1 obtain ⟨x₀, hx₀, hmax⟩ := isCompact_Icc.exists_isMaxOn (Set.nonempty_Icc.mpr hab.le) hf let B : ℝ := f x₀ + 1 have hB : 0 < B := by have : 0 ≤ f x₀ := Real.sqrt_nonneg _ dsimp [B]; linarith have hupper : ∀ x ∈ Icc a b, f x ≤ B := by intro x hx exact (hmax hx).trans (by dsimp [B]; linarith) let δ : ℝ := min 1 (η / (2 * B + 1)) have hδ : 0 < δ := lt_min_iff.mpr ⟨by norm_num, div_pos hη (by linarith)⟩ obtain ⟨K, hK⟩ := companding_midpoint_mass_error_eventually a b hab S hS β hcont hpos δ hδ refine ⟨K, ?_⟩ intro k hkK hk j let l := boundary a b S k j.val β let r := boundary a b S k (j.val + 1) β let m := (l + r) / 2 let L := r - l let q := f m * L let t := (∫ x in a..b, f x) / k have hmem : m ∈ Icc a b := by have hl := (boundary_equal_mass a b hab S k j.val hS hk j.isLt.le β hcont hpos).1 have hr := (boundary_equal_mass a b hab S k (j.val + 1) hS hk (by omega) β hcont hpos).1 dsimp [m] constructor <;> linarith [hl.1, hl.2, hr.1, hr.2] have hL : 0 ≤ L := by dsimp [L] exact sub_nonneg.mpr (((boundary_order a b hab S k hS hk β hcont hpos).2.2 j.val (j.val + 1) (by omega) (by omega)).le) have hq : 0 ≤ q := mul_nonneg (Real.sqrt_nonneg _) hL have hqB : q ≤ B * L := mul_le_mul_of_nonneg_right (hupper m hmem) hL have he : |q - t| ≤ δ * L := hK k hkK hk j have ht : 0 ≤ t := by have hM := (sqrt_mass_regular a b hab S hS β hcont hpos).2 exact div_nonneg hM.le (by exact_mod_cast (zero_le k)) have htB : t ≤ (B + δ) * L := by have := (abs_le.mp he).1 nlinarith have hδone : δ ≤ 1 := min_le_left _ _ have hδeta : δ * (2 * B + 1) ≤ η := by have h := min_le_right (1 : ℝ) (η / (2 * B + 1)) exact (le_div_iff₀ (by linarith : 0 < 2 * B + 1)).mp h have hdiag : 0 ≤ diagonalWeight S β m := ((diagonal_regular a b S hS β hcont hpos).2 m hmem).le have hsq : diagonalWeight S β m * L ^ 2 = q ^ 2 := by calc _ = (sqrt (diagonalWeight S β m)) ^ 2 * L ^ 2 := by rw [Real.sq_sqrt hdiag] _ = q ^ 2 := by dsimp [q, f]; ring change |diagonalWeight S β m * L ^ 2 - t ^ 2| ≤ η * L ^ 2 rw [hsq, show q ^ 2 - t ^ 2 = (q - t) * (q + t) by ring, abs_mul, abs_of_nonneg (add_nonneg hq ht)] have hsum : q + t ≤ (2 * B + 1) * L := by nlinarith have hprod := mul_le_mul he hsum (add_nonneg hq ht) (mul_nonneg hδ.le hL) have hlast : (δ * L) * ((2 * B + 1) * L) ≤ η * L ^ 2 := by nlinarith [mul_nonneg (sub_nonneg.mpr hδeta) (sq_nonneg L)] exact hprod.trans hlast -
companding_integrand_cell_error_eventuallytheorem — The true paired cost of one sufficiently fine companding cell differs from its midpoint diagonal-weight surrogate by at most a prescribed multiple of that cell's squared length.hypothesesconclusion∃ K : ℕ,∀ k : ℕ,K≤ k → 0 < k → ∀ j : Fin k, |(∑ s : Fin S, ∫ x in compandingCell a b S k β j, β s x (compandingMidpoint a b S k β j s) * |x - compandingMidpoint a b S k β j s|)- diagonalWeight S β ((boundary a b S k j.val β + boundary a b S k (j.val + 1) β) / 2) * (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) ^ 2 / 4|Proof (Lean source)
theorem companding_integrand_cell_error_eventually (a b : ℝ) (hab : a < b) (S : ℕ) (hS : 0 < S) (β : Fin S → ℝ → ℝ → ℝ) (hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2) (Icc a b ×ˢ Icc a b)) (hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z) : ∀ η : ℝ, 0 < η → ∃ K : ℕ, ∀ k : ℕ, K ≤ k → 0 < k → ∀ j : Fin k, |(∑ s : Fin S, ∫ x in compandingCell a b S k β j, β s x (compandingMidpoint a b S k β j s) * |x - compandingMidpoint a b S k β j s|) - diagonalWeight S β ((boundary a b S k j.val β + boundary a b S k (j.val + 1) β) / 2) * (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) ^ 2 / 4| ≤ η * (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) ^ 2 := by classical intro η hη let δ : ℝ := 4 * η / S have hSreal : (0 : ℝ) < S := by exact_mod_cast hS have hδ : 0 < δ := div_pos (by positivity) hSreal obtain ⟨K, hK⟩ := companding_coefficient_error_eventually a b hab S hS β hcont hpos δ hδ refine ⟨K, ?_⟩ intro k hkK hk j let C := compandingCell a b S k β j let m := (boundary a b S k j.val β + boundary a b S k (j.val + 1) β) / 2 let L := boundary a b S k (j.val + 1) β - boundary a b S k j.val β let H := L ^ 2 / 4 have hH : 0 ≤ H := by dsimp [H]; positivity obtain ⟨hpart, hmid⟩ := companding_feasible a b hab S k hS hk β hcont hpos have hCmeas : MeasurableSet C := hpart.1 j have hCsub : C ⊆ Icc a b := by intro x hx rw [← hpart.2.2] exact Set.mem_iUnion.mpr ⟨j, hx⟩ have hm : m ∈ Icc a b := by simpa only [m, compandingMidpoint] using hmid j ⟨0, hS⟩ have hdistInt : IntegrableOn (fun x => |x - m|) C volume := by have hcont' : Continuous (fun x : ℝ => |x - m|) := by fun_prop exact (hcont'.continuousOn.integrableOn_compact isCompact_Icc).mono_set hCsub have hmoment : (∫ x in C, |x - m|) = H := by simpa only [C, m, H, compandingMidpoint] using (companding_cell_midpoint_moment a b hab S k hS hk β hcont hpos j ⟨0, hS⟩) have hconst (v : ℝ) : (∫ x in C, v * |x - m|) = v * H := by rw [integral_const_mul, hmoment] have hone (s : Fin S) : |(∫ x in C, β s x m * |x - m|) - β s m m * H| ≤ δ * H := by have hInt : IntegrableOn (fun x => β s x m * |x - m|) C volume := weighted_cell_integrable a b (β s) (hcont s) C hCsub m hm have hpoint (x : ℝ) (hx : x ∈ C) : |β s x m - β s m m| ≤ δ := by simpa only [C, m, compandingMidpoint] using hK k hkK hk j s x hx have hlow : (β s m m - δ) * H ≤ ∫ x in C, β s x m * |x - m| := by rw [← hconst] apply setIntegral_mono_on (hdistInt.const_mul _) hInt hCmeas intro x hx apply mul_le_mul_of_nonneg_right _ (abs_nonneg _) linarith [(abs_le.mp (hpoint x hx)).1] have hupp : (∫ x in C, β s x m * |x - m|) ≤ (β s m m + δ) * H := by rw [← hconst] apply setIntegral_mono_on hInt (hdistInt.const_mul _) hCmeas intro x hx apply mul_le_mul_of_nonneg_right _ (abs_nonneg _) linarith [(abs_le.mp (hpoint x hx)).2] exact abs_le.mpr ⟨by nlinarith, by nlinarith⟩ have hsum : |(∑ s : Fin S, ∫ x in C, β s x m * |x - m|) - diagonalWeight S β m * H| ≤ (S : ℝ) * (δ * H) := by rw [diagonalWeight, Finset.sum_mul, ← Finset.sum_sub_distrib] calc _ ≤ ∑ s : Fin S, |(∫ x in C, β s x m * |x - m|) - β s m m * H| := Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ _s : Fin S, δ * H := Finset.sum_le_sum (fun s _ => hone s) _ = (S : ℝ) * (δ * H) := by simp have hgoal : |(∑ s : Fin S, ∫ x in C, β s x m * |x - m|) - diagonalWeight S β m * H| ≤ η * L ^ 2 := by calc _ ≤ (S : ℝ) * (δ * H) := hsum _ = η * L ^ 2 := by dsimp [δ, H]; field_simp simpa only [C, m, L, H, compandingMidpoint, mul_div_assoc] using hgoal -
companding_surrogate_scaled_tendstotheorem — The scaled midpoint diagonal-weight surrogate converges to one quarter of the squared total square-root diagonal mass.hypothesesconclusionTendsto (fun k : ℕ => (k : ℝ) * compandingSurrogateCost a b S k β) atTop (nhds ((1 / 4 : ℝ) * (∫ x in a..b, sqrt (diagonalWeight S β x)) ^ 2))Proof (Lean source)
theorem companding_surrogate_scaled_tendsto (a b : ℝ) (hab : a < b) (S : ℕ) (hS : 0 < S) (β : Fin S → ℝ → ℝ → ℝ) (hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2) (Icc a b ×ˢ Icc a b)) (hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z) : Tendsto (fun k : ℕ => (k : ℝ) * compandingSurrogateCost a b S k β) atTop (nhds ((1 / 4 : ℝ) * (∫ x in a..b, sqrt (diagonalWeight S β x)) ^ 2)) := by classical obtain ⟨C, hC, hbound⟩ := companding_scaled_length_square_bound a b hab S hS β hcont hpos let M : ℝ := ∫ x in a..b, sqrt (diagonalWeight S β x) apply Metric.tendsto_atTop.mpr intro ε hε let η : ℝ := 4 * ε / (C + 1) have hη : 0 < η := by dsimp [η]; positivity obtain ⟨K, hK⟩ := companding_surrogate_cell_error_eventually a b hab S hS β hcont hpos η hη refine ⟨max K 1, ?_⟩ intro k hk have hkK : K ≤ k := le_trans (le_max_left _ _) hk have hkpos : 0 < k := lt_of_lt_of_le (by omega : 0 < max K 1) hk have hkreal : (0 : ℝ) < k := by exact_mod_cast hkpos have hcell (j : Fin k) : |diagonalWeight S β ((boundary a b S k j.val β + boundary a b S k (j.val + 1) β) / 2) * (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) ^ 2 - (M / k) ^ 2| ≤ η * (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) ^ 2 := hK k hkK hkpos j have hsum : |∑ j : Fin k, (diagonalWeight S β ((boundary a b S k j.val β + boundary a b S k (j.val + 1) β) / 2) * (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) ^ 2 - (M / k) ^ 2)| ≤ η * ∑ j : Fin k, (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) ^ 2 := by calc _ ≤ ∑ j : Fin k, |diagonalWeight S β ((boundary a b S k j.val β + boundary a b S k (j.val + 1) β) / 2) * (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) ^ 2 - (M / k) ^ 2| := Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ j : Fin k, η * (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) ^ 2 := Finset.sum_le_sum (fun j _ => hcell j) _ = _ := by rw [Finset.mul_sum] have hid : (k : ℝ) * compandingSurrogateCost a b S k β - M ^ 2 / 4 = ((k : ℝ) / 4) * ∑ j : Fin k, (diagonalWeight S β ((boundary a b S k j.val β + boundary a b S k (j.val + 1) β) / 2) * (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) ^ 2 - (M / k) ^ 2) := by simp only [compandingSurrogateCost, Finset.sum_sub_distrib, Finset.sum_const, Finset.card_fin, nsmul_eq_mul] rw [mul_sub] congr 1 · conv_lhs => rw [Finset.mul_sum] conv_rhs => rw [Finset.mul_sum] apply Finset.sum_congr rfl intro j hj ring · field_simp have hfinal : |(k : ℝ) * compandingSurrogateCost a b S k β - M ^ 2 / 4| ≤ η * C / 4 := by rw [hid, abs_mul, abs_of_nonneg (div_nonneg hkreal.le (by norm_num))] have hb := hbound k hkpos have hp := mul_le_mul_of_nonneg_left hsum (show 0 ≤ (k : ℝ) / 4 by positivity) nlinarith [mul_nonneg hη.le (sub_nonneg.mpr hb)] have hsmall : η * C / 4 < ε := by have hratio : C / (C + 1) < 1 := (div_lt_iff₀ (by linarith : 0 < C + 1)).2 (by linarith) calc η * C / 4 = ε * (C / (C + 1)) := by dsimp [η]; ring _ < ε * 1 := mul_lt_mul_of_pos_left hratio hε _ = ε := by ring have hquarter : (1 / 4 : ℝ) * M ^ 2 = M ^ 2 / 4 := by ring rw [Real.dist_eq, hquarter] exact lt_of_le_of_lt hfinal hsmall -
companding_surrogate_error_tendstotheorem — The scaled difference between the true paired midpoint cost and its diagonal-weight surrogate tends to zero as the companding mesh vanishes.hypothesesconclusionTendsto (fun k : ℕ => (k : ℝ) * (weightedCost S k β (compandingCell a b S k β) (compandingMidpoint a b S k β) - compandingSurrogateCost a b S k β)) atTop (nhds 0)Proof (Lean source)
theorem companding_surrogate_error_tendsto (a b : ℝ) (hab : a < b) (S : ℕ) (hS : 0 < S) (β : Fin S → ℝ → ℝ → ℝ) (hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2) (Icc a b ×ˢ Icc a b)) (hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z) : Tendsto (fun k : ℕ => (k : ℝ) * (weightedCost S k β (compandingCell a b S k β) (compandingMidpoint a b S k β) - compandingSurrogateCost a b S k β)) atTop (nhds 0) := by classical obtain ⟨C, hC, hbound⟩ := companding_scaled_length_square_bound a b hab S hS β hcont hpos apply Metric.tendsto_atTop.mpr intro ε hε let η : ℝ := ε / (C + 1) have hη : 0 < η := by dsimp [η]; positivity obtain ⟨K, hK⟩ := companding_integrand_cell_error_eventually a b hab S hS β hcont hpos η hη refine ⟨max K 1, ?_⟩ intro k hk have hkK : K ≤ k := le_trans (le_max_left _ _) hk have hkpos : 0 < k := lt_of_lt_of_le (by omega : 0 < max K 1) hk have hkreal : (0 : ℝ) ≤ k := by exact_mod_cast (zero_le k) have hsum : |∑ j : Fin k, ((∑ s : Fin S, ∫ x in compandingCell a b S k β j, β s x (compandingMidpoint a b S k β j s) * |x - compandingMidpoint a b S k β j s|) - diagonalWeight S β ((boundary a b S k j.val β + boundary a b S k (j.val + 1) β) / 2) * (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) ^ 2 / 4)| ≤ η * ∑ j : Fin k, (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) ^ 2 := by calc _ ≤ ∑ j : Fin k, |(∑ s : Fin S, ∫ x in compandingCell a b S k β j, β s x (compandingMidpoint a b S k β j s) * |x - compandingMidpoint a b S k β j s|) - diagonalWeight S β ((boundary a b S k j.val β + boundary a b S k (j.val + 1) β) / 2) * (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) ^ 2 / 4| := Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ j : Fin k, η * (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) ^ 2 := Finset.sum_le_sum (fun j _ => hK k hkK hkpos j) _ = _ := by rw [Finset.mul_sum] have hid : weightedCost S k β (compandingCell a b S k β) (compandingMidpoint a b S k β) - compandingSurrogateCost a b S k β = ∑ j : Fin k, ((∑ s : Fin S, ∫ x in compandingCell a b S k β j, β s x (compandingMidpoint a b S k β j s) * |x - compandingMidpoint a b S k β j s|) - diagonalWeight S β ((boundary a b S k j.val β + boundary a b S k (j.val + 1) β) / 2) * (boundary a b S k (j.val + 1) β - boundary a b S k j.val β) ^ 2 / 4) := by simp only [weightedCost, compandingSurrogateCost, Finset.sum_sub_distrib] rw [Real.dist_eq, sub_zero, abs_mul, abs_of_nonneg hkreal, hid] have hb := hbound k hkpos have hp := mul_le_mul_of_nonneg_left hsum hkreal have hsmall : η * C < ε := by have hratio : C / (C + 1) < 1 := (div_lt_iff₀ (by linarith : 0 < C + 1)).2 (by linarith) calc η * C = ε * (C / (C + 1)) := by dsimp [η]; ring _ < ε * 1 := mul_lt_mul_of_pos_left hratio hε _ = ε := by ring exact lt_of_le_of_lt (by nlinarith [mul_nonneg hη.le (sub_nonneg.mpr hb)]) hsmall
Lower 1 core · 3 supporting Uniform high-rate lower bounds over all finite measurable partitions, including disconnected cells and separate reproduction points. ★ arbitrary_partition_lower_eventually
Uniform high-rate lower bounds over all finite measurable partitions, including disconnected cells and separate reproduction points.
theorem arbitrary_partition_lower_eventually reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Quantization
On a nondegenerate interval from a to b, for a nonempty finite weight family with continuous strictly positive weights, for every positive tolerance ε there is a cell count K such that, for every k ≥ K, every measurable partition of the interval into k cells and every array of reproduction points in the interval, k times the paired weighted cost is at least one quarter of the square of the integral of the square root of the diagonal weight, minus ε.
Formal statement
hypotheses
conclusion
∃ K : ℕ,
∀ k : ℕ,
K
≤ k → 0 < k → ∀ (B : Fin k → Set ℝ) (z : Fin k → Fin S → ℝ), IsMeasurablePartition a b k B → (∀ j s, z j s ∈ Icc a b) → (1 / 4 : ℝ) * (∫ x in a..b, sqrt (diagonalWeight S β x)) ^ 2
- ε ≤ (k : ℝ) * weightedCost S k β B z
Proof (Lean source)
theorem arbitrary_partition_lower_eventually (a b : ℝ) (hab : a < b)
(S : ℕ) (hS : 0 < S) (β : Fin S → ℝ → ℝ → ℝ)
(hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2)
(Icc a b ×ˢ Icc a b))
(hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z) :
∀ ε : ℝ, 0 < ε → ∃ K : ℕ, ∀ k : ℕ, K ≤ k → 0 < k →
∀ (B : Fin k → Set ℝ) (z : Fin k → Fin S → ℝ),
IsMeasurablePartition a b k B →
(∀ j s, z j s ∈ Icc a b) →
(1 / 4 : ℝ) *
(∫ x in a..b, sqrt (diagonalWeight S β x)) ^ 2 - ε ≤
(k : ℝ) * weightedCost S k β B z := by
-- Let A = (∫ sqrt w)^2/4. For fixed ε, choose η∈(0,1) so that
-- (1-η)*A is close to A, and obtain δ from partition_good_mass_lower.
-- Candidates with k*cost greater than A satisfy the goal directly.
-- For the others, bad_region_mass_small_of_scaled_cost_bound makes the
-- removed square-root mass uniformly small for large k. Positivity of
-- ∫ sqrt w and the bad-mass integrals then converts the aggregate
-- quarter-square estimate into A-ε ≤ k*cost.
intro ε hε
let I : ℝ := ∫ x in a..b, sqrt (diagonalWeight S β x)
let A : ℝ := I ^ 2 / 4
have hI : 0 < I := (sqrt_mass_regular a b hab S hS β hcont hpos).2
have hA : 0 ≤ A := by dsimp [A]; positivity
let η : ℝ := ε / (ε + I ^ 2 + 1)
have hηden : 0 < ε + I ^ 2 + 1 := by positivity
have hη : 0 < η := div_pos hε hηden
have hη1 : η < 1 := by
apply (div_lt_iff₀ hηden).2
nlinarith [sq_nonneg I]
have hηbound : η * I ^ 2 ≤ ε := by
have hsq : I ^ 2 ≤ ε + I ^ 2 + 1 := by linarith
calc
η * I ^ 2 ≤ η * (ε + I ^ 2 + 1) :=
mul_le_mul_of_nonneg_left hsq hη.le
_ = ε := by dsimp [η]; field_simp
let t : ℝ := ε / (ε + I + 1)
have htden : 0 < ε + I + 1 := by positivity
have ht : 0 < t := div_pos hε htden
have htbound : I * t ≤ ε := by
have hle : I ≤ ε + I + 1 := by linarith
calc
I * t ≤ (ε + I + 1) * t :=
mul_le_mul_of_nonneg_right hle ht.le
_ = ε := by dsimp [t]; field_simp
obtain ⟨δ, hδ, hagg⟩ :=
partition_good_mass_lower a b hab S hS β hcont hpos η hη hη1
obtain ⟨K, hK⟩ :=
bad_region_mass_small_of_scaled_cost_bound a b hab S hS β hcont hpos
δ A t hδ ht
refine ⟨K, ?_⟩
intro k hkK hk B z hB hz
let bad : ℝ := ∑ j : Fin k,
∫ x in badRegion S k δ B z j,
sqrt (diagonalWeight S β x)
by_cases hlarge : A ≤ (k : ℝ) * weightedCost S k β B z
· dsimp [A, I] at hlarge ⊢
linarith
have hcost : (k : ℝ) * weightedCost S k β B z ≤ A :=
le_of_lt (lt_of_not_ge hlarge)
have hbad : bad ≤ t := hK k hkK hk B z hB hz hcost
have hbadnonneg : 0 ≤ bad := by
dsimp [bad]
apply Finset.sum_nonneg
intro j hj
exact integral_nonneg (fun x => Real.sqrt_nonneg _)
have hIbad : I * bad ≤ ε :=
(mul_le_mul_of_nonneg_left hbad hI.le).trans htbound
have hagg' : (1 - η) * (I - bad) ^ 2 / 4 ≤
(k : ℝ) * weightedCost S k β B z := by
simpa only [I, bad] using hagg k hk B z hB hz
have hsq : 0 ≤ (1 - η) * bad ^ 2 :=
mul_nonneg (sub_nonneg.mpr hη1.le) (sq_nonneg bad)
have hcross : 0 ≤ η * I * bad :=
mul_nonneg (mul_nonneg hη.le hI.le) hbadnonneg
have hgoal : A - ε ≤ (k : ℝ) * weightedCost S k β B z := by
dsimp [A]
nlinarith
convert hgoal using 1 <;> dsimp [A, I] <;> ring
3 supporting declarations (lemmas, instances)
-
measurable_partition_mass_square_lowertheorem — In any measurable partition of [a,b] into k cells, the sum of squared cell masses is at least the squared interval length divided by k.hypothesesconclusion(b - a) ^ 2 ≤ (k : ℝ) * ∑ j : Fin k, (volume.real (B j)) ^ 2Proof (Lean source)
theorem measurable_partition_mass_square_lower (a b : ℝ) (hab : a ≤ b) (k : ℕ) (B : Fin k → Set ℝ) (hB : IsMeasurablePartition a b k B) : (b - a) ^ 2 ≤ (k : ℝ) * ∑ j : Fin k, (volume.real (B j)) ^ 2 := by -- Add the masses of the disjoint cells, then apply finite Cauchy-Schwarz -- to their sum. Each cell has finite measure because it lies in Icc a b. have hsub (j : Fin k) : B j ⊆ Icc a b := by intro x hx rw [← hB.2.2] exact Set.mem_iUnion.2 ⟨j, hx⟩ have hfin (j : Fin k) : volume (B j) ≠ ⊤ := (measure_lt_top_of_subset (hsub j) (measure_Icc_lt_top (μ := volume)).ne).ne have hsum : ∑ j : Fin k, volume.real (B j) = b - a := by rw [← measureReal_iUnion_fintype (fun i j hij => hB.2.1 i j hij) hB.1 hfin, hB.2.2, Real.volume_real_Icc_of_le hab] rw [← hsum] simpa using (sq_sum_le_card_mul_sum_sq (s := univ) (f := fun j : Fin k => volume.real (B j))) -
constant_weights_partition_lowertheorem — For constant nonnegative coefficients, every measurable partition and separate reproduction array obey the exact quarter-square lower bound.hypothesesconclusion(∑ s : Fin S, γ s) * (b - a) ^ 2 / 4 ≤ (k : ℝ) * weightedCost S k (fun s _ _ => γ s) B zProof (Lean source)
theorem constant_weights_partition_lower (a b : ℝ) (hab : a ≤ b) (S k : ℕ) (γ : Fin S → ℝ) (hγ : ∀ s, 0 ≤ γ s) (B : Fin k → Set ℝ) (z : Fin k → Fin S → ℝ) (hB : IsMeasurablePartition a b k B) : (∑ s : Fin S, γ s) * (b - a) ^ 2 / 4 ≤ (k : ℝ) * weightedCost S k (fun s _ _ => γ s) B z := by -- Sum weighted_measurable_cell_moment over cells and combine with -- measurable_partition_mass_square_lower. No interval-cell assumption. have hsub (j : Fin k) : B j ⊆ Icc a b := by intro x hx rw [← hB.2.2] exact Set.mem_iUnion.2 ⟨j, hx⟩ have hmass := measurable_partition_mass_square_lower a b hab k B hB have hγsum : 0 ≤ ∑ s : Fin S, γ s := Finset.sum_nonneg (fun s _ => hγ s) have hkreal : (0 : ℝ) ≤ k := Nat.cast_nonneg _ calc (∑ s : Fin S, γ s) * (b - a) ^ 2 / 4 ≤ (∑ s : Fin S, γ s) * ((k : ℝ) * ∑ j : Fin k, (volume.real (B j)) ^ 2) / 4 := by gcongr _ = (k : ℝ) * ∑ j : Fin k, ((∑ s : Fin S, γ s) * (volume.real (B j)) ^ 2 / 4) := by rw [← Finset.sum_div, ← Finset.mul_sum] ring _ ≤ (k : ℝ) * ∑ j : Fin k, ∑ s : Fin S, γ s * (∫ x in B j, |x - z j s|) := by apply mul_le_mul_of_nonneg_left _ hkreal apply Finset.sum_le_sum intro j hj exact weighted_measurable_cell_moment a b hab (B j) (hB.1 j) (hsub j) S γ hγ (z j) _ = (k : ℝ) * weightedCost S k (fun s _ _ => γ s) B z := by simp only [weightedCost, integral_const_mul] -
optimal_lower_eventuallytheorem — The same universal lower bound holds for the optimal value, since the feasible cost set is nonempty and all its members obey the uniform estimate.hypothesesconclusion∃ K : ℕ,∀ k : ℕ,K≤ k → 0 < k → (1 / 4 : ℝ) * (∫ x in a..b, sqrt (diagonalWeight S β x)) ^ 2- ε ≤ (k : ℝ) * optimalCost a b S k βProof (Lean source)
theorem optimal_lower_eventually (a b : ℝ) (hab : a < b) (S : ℕ) (hS : 0 < S) (β : Fin S → ℝ → ℝ → ℝ) (hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2) (Icc a b ×ˢ Icc a b)) (hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z) : ∀ ε : ℝ, 0 < ε → ∃ K : ℕ, ∀ k : ℕ, K ≤ k → 0 < k → (1 / 4 : ℝ) * (∫ x in a..b, sqrt (diagonalWeight S β x)) ^ 2 - ε ≤ (k : ℝ) * optimalCost a b S k β := by -- Use arbitrary_partition_lower_eventually and le_csInf; the feasible -- companding code witnesses nonemptiness of the cost set. intro ε hε obtain ⟨K, hK⟩ := arbitrary_partition_lower_eventually a b hab S hS β hcont hpos ε hε refine ⟨K, ?_⟩ intro k hkK hk have hkreal : (0 : ℝ) < k := Nat.cast_pos.mpr hk have hfeas := companding_feasible a b hab S k hS hk β hcont hpos have hne : {v : ℝ | ∃ (B : Fin k → Set ℝ) (z : Fin k → Fin S → ℝ), IsMeasurablePartition a b k B ∧ (∀ j s, z j s ∈ Icc a b) ∧ v = weightedCost S k β B z}.Nonempty := by exact ⟨weightedCost S k β (compandingCell a b S k β) (compandingMidpoint a b S k β), compandingCell a b S k β, compandingMidpoint a b S k β, hfeas.1, hfeas.2, rfl⟩ let A : ℝ := (1 / 4 : ℝ) * (∫ x in a..b, sqrt (diagonalWeight S β x)) ^ 2 have hlim : (A - ε) / (k : ℝ) ≤ optimalCost a b S k β := by unfold optimalCost apply le_csInf hne rintro v ⟨B, z, hB, hz, rfl⟩ apply (div_le_iff₀ hkreal).2 simpa only [mul_comm] using hK k hkK hk B z hB hz calc A - ε = (k : ℝ) * ((A - ε) / (k : ℝ)) := by field_simp _ ≤ (k : ℝ) * optimalCost a b S k β := mul_le_mul_of_nonneg_left hlim hkreal.le
LowerAggregate 1 core · 0 supporting Aggregation of local good-cell moment estimates over a measurable partition. ★ partition_good_mass_lower
Aggregation of local good-cell moment estimates over a measurable partition. Bad regions are retained explicitly as a mass deficit.
theorem partition_good_mass_lower reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Quantization
On a nondegenerate interval from a to b, for a nonempty finite weight family with continuous strictly positive weights, for every relative error η strictly between zero and one there is a positive radius δ such that, for every positive cell count k, every measurable partition into k cells and every array of reproduction points in the interval, k times the paired weighted cost is at least (1 − η)/4 times the square of the total square-root diagonal mass of the interval minus the square-root diagonal mass of the radius-δ bad regions of all cells.
Formal statement
hypotheses
conclusion
∃ δ : ℝ,
0 < δ
conclusion 1
(1 - η) * ((∫ x in a..b, sqrt (diagonalWeight S β x)) - ∑ j : Fin k, ∫ x in badRegion S k δ B z j, sqrt (diagonalWeight S β x)) ^ 2 / 4
≤ (k : ℝ) * weightedCost S k β B z
Proof (Lean source)
theorem partition_good_mass_lower (a b : ℝ) (hab : a < b)
(S : ℕ) (hS : 0 < S) (β : Fin S → ℝ → ℝ → ℝ)
(hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2)
(Icc a b ×ˢ Icc a b))
(hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z) :
∀ η : ℝ, 0 < η → η < 1 → ∃ δ : ℝ, 0 < δ ∧
∀ k : ℕ, 0 < k →
∀ (B : Fin k → Set ℝ) (z : Fin k → Fin S → ℝ),
IsMeasurablePartition a b k B →
(∀ j s, z j s ∈ Icc a b) →
(1 - η) *
((∫ x in a..b, sqrt (diagonalWeight S β x)) -
∑ j : Fin k,
∫ x in badRegion S k δ B z j,
sqrt (diagonalWeight S β x)) ^ 2 / 4 ≤
(k : ℝ) * weightedCost S k β B z := by
-- Apply partition_good_square_sum_lower to the good cells, then finite
-- Cauchy-Schwarz to their masses. Use partition_good_mass_identity to
-- identify the sum of those masses with total mass minus bad mass.
intro η hη hη1
obtain ⟨δ, hδ, hsum⟩ :=
partition_good_square_sum_lower a b hab S hS β hcont hpos η hη hη1
refine ⟨δ, hδ, ?_⟩
intro k hk B z hB hz
let m : Fin k → ℝ := fun j =>
∫ x in B j \ badRegion S k δ B z j,
sqrt (diagonalWeight S β x)
have hcs : (∑ j : Fin k, m j) ^ 2 ≤
(k : ℝ) * ∑ j : Fin k, (m j) ^ 2 := by
simpa [m] using (sq_sum_le_card_mul_sum_sq (s := univ) (f := m))
have hfactor : 0 ≤ (1 - η) / 4 := by
have : 0 ≤ 1 - η := sub_nonneg.mpr hη1.le
positivity
have hid := partition_good_mass_identity a b hab S k hS β hcont hpos B z hB δ
calc
(1 - η) *
((∫ x in a..b, sqrt (diagonalWeight S β x)) -
∑ j : Fin k,
∫ x in badRegion S k δ B z j,
sqrt (diagonalWeight S β x)) ^ 2 / 4 =
(1 - η) / 4 * (∑ j : Fin k, m j) ^ 2 := by
rw [hid]
ring
_ ≤ (1 - η) / 4 * ((k : ℝ) * ∑ j : Fin k, (m j) ^ 2) :=
mul_le_mul_of_nonneg_left hcs hfactor
_ = (k : ℝ) * ((1 - η) *
(∑ j : Fin k, (m j) ^ 2) / 4) := by ring
_ ≤ (k : ℝ) * weightedCost S k β B z := by
apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg k)
simpa [m] using hsum k hk B z hB hz
LowerGeometry 1 core · 1 supporting Pointwise geometry used to control arbitrary measurable cells in the universal lower bound. ★ good_cell_diameter
Pointwise geometry used to control arbitrary measurable cells in the universal lower bound. No cell is assumed to be connected.
theorem good_cell_diameter reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Quantization
A nonempty index family with reproduction points and two source points each close to every reproduction has source-point distance at most twice the common radius.
Formal statement
hypotheses
conclusion
|x - y| ≤ 2 * δ
Proof (Lean source)
theorem good_cell_diameter (S : ℕ) (hS : 0 < S) (z : Fin S → ℝ)
(x y δ : ℝ) (hx : ∀ s, |x - z s| ≤ δ)
(hy : ∀ s, |y - z s| ≤ δ) :
|x - y| ≤ 2 * δ := by
let s : Fin S := ⟨0, hS⟩
calc
|x - y| = |(x - z s) + (z s - y)| := by ring
_ ≤ |x - z s| + |z s - y| := abs_add_le _ _
_ ≤ δ + δ := add_le_add (hx s) (by simpa [abs_sub_comm] using hy s)
_ = 2 * δ := by ring
1 supporting declaration (lemmas, instances)
-
far_point_cost_lowertheorem — If a source point lies at least δ from one reproduction point and all weights there are at least c, its paired distortion is at least c*δ.hypothesesS :ℕβ :Fin S → ℝ → ℝ → ℝz :Fin S → ℝx c δ :ℝhc :0 ≤ chδ :0 ≤ δhβ :∀ s, c ≤ β s x (z s)hfar :∃ s, δ ≤ |x - z s|conclusionc * δ ≤ ∑ s : Fin S, β s x (z s) * |x - z s|Proof (Lean source)
theorem far_point_cost_lower (S : ℕ) (β : Fin S → ℝ → ℝ → ℝ) (z : Fin S → ℝ) (x c δ : ℝ) (hc : 0 ≤ c) (hδ : 0 ≤ δ) (hβ : ∀ s, c ≤ β s x (z s)) (hfar : ∃ s, δ ≤ |x - z s|) : c * δ ≤ ∑ s : Fin S, β s x (z s) * |x - z s| := by obtain ⟨s, hs⟩ := hfar have hsingle : c * δ ≤ β s x (z s) * |x - z s| := mul_le_mul (hβ s) hs hδ (hc.trans (hβ s)) have hnonneg : ∀ t : Fin S, 0 ≤ β t x (z t) * |x - z t| := by intro t exact mul_nonneg (hc.trans (hβ t)) (abs_nonneg _) exact hsingle.trans (Finset.single_le_sum (fun t _ => hnonneg t) (Finset.mem_univ s))
LowerGood 1 core · 3 supporting Local square-root-mass estimates for arbitrary measurable parts of a quantization cell. ★ good_cell_sqrt_mass_lower
Local square-root-mass estimates for arbitrary measurable parts of a quantization cell. These estimates require no interval shape or connectedness.
theorem good_cell_sqrt_mass_lower reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Quantization
On a nondegenerate interval from a to b, for a nonempty finite weight family with continuous strictly positive weights, for every relative error η strictly between zero and one there is a positive radius δ such that, for every measurable cell B inside the interval, every measurable part G of B, and every family of reproduction points z_s in the interval all within δ of every point of G, the sum over s of the integral over B of β_s(x, z_s)·|x − z_s| is at least (1 − η)/4 times the square of the integral over G of the square root of the diagonal weight.
Formal statement
hypotheses
Proof (Lean source)
theorem good_cell_sqrt_mass_lower (a b : ℝ) (hab : a < b)
(S : ℕ) (hS : 0 < S) (β : Fin S → ℝ → ℝ → ℝ)
(hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2)
(Icc a b ×ˢ Icc a b))
(hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z) :
∀ η : ℝ, 0 < η → η < 1 → ∃ δ : ℝ, 0 < δ ∧
∀ (B G : Set ℝ) (z : Fin S → ℝ),
MeasurableSet B → MeasurableSet G →
B ⊆ Icc a b → G ⊆ B →
(∀ s, z s ∈ Icc a b) →
(∀ x ∈ G, ∀ s, |x - z s| ≤ δ) →
(1 - η) * (∫ x in G, sqrt (diagonalWeight S β x)) ^ 2 / 4 ≤
∑ s : Fin S, ∫ x in B, β s x (z s) * |x - z s| := by
-- For nonempty G choose x₀∈G. Obtain one γ,Q for every x∈G from
-- good_cell_relative_freeze, then apply frozen_cell_sqrt_mass_lower.
-- The empty G case follows from cost nonnegativity.
intro η hη hη1
obtain ⟨δ, hδ, hfreeze⟩ :=
good_cell_relative_freeze a b hab S hS β hcont hpos η hη hη1
refine ⟨δ, hδ, ?_⟩
intro B G z hB hG hsub hGB hz hnear
have hnonneg : ∀ x ∈ B, ∀ s, 0 ≤ β s x (z s) := by
intro x hx s
exact (hpos s x (z s) (hsub hx) (hz s)).le
have hInt : ∀ s, IntegrableOn (fun x => β s x (z s) * |x - z s|) B volume := by
intro s
exact weighted_cell_integrable a b (β s) (hcont s)
B hsub (z s) (hz s)
by_cases hne : G.Nonempty
· obtain ⟨y, hy⟩ := hne
obtain ⟨γ, Q, hγ, hQ, hcoeff, hpoint⟩ :=
hfreeze y z (hsub (hGB hy)) hz (hnear y hy)
apply frozen_cell_sqrt_mass_lower a b hab.le S β B G hB hG hsub hGB
z γ hγ _ hnonneg hInt Q η hQ ⟨hη.le, hη1⟩ _ hcoeff
· intro x hx s
exact (hpoint x (hsub (hGB hx)) (hnear x hx)).1 s
· intro x hx
exact (hpoint x (hsub (hGB hx)) (hnear x hx)).2
· have hempty : G = ∅ := Set.not_nonempty_iff_eq_empty.mp hne
simp only [hempty, setIntegral_empty, zero_pow (by decide : (2 : ℕ) ≠ 0),
mul_zero, zero_div]
apply Finset.sum_nonneg
intro s hs
apply setIntegral_nonneg hB
intro x hx
exact mul_nonneg (hnonneg x hx s) (abs_nonneg _)
3 supporting declarations (lemmas, instances)
-
good_cell_uniform_freezetheorem — On a sufficiently small good part of a cell, every actual coefficient is uniformly close to the diagonal coefficient at any anchor point in that part, and the square-root diagonal density is uniformly close at the same two points. The radius works for all reproduction arrays in the source interval.hypothesesProof (Lean source)
theorem good_cell_uniform_freeze (a b : ℝ) (hab : a < b) (S : ℕ) (hS : 0 < S) (β : Fin S → ℝ → ℝ → ℝ) (hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2) (Icc a b ×ˢ Icc a b)) (hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z) : ∀ ε : ℝ, 0 < ε → ∃ δ : ℝ, 0 < δ ∧ ∀ (x y : ℝ) (z : Fin S → ℝ), x ∈ Icc a b → y ∈ Icc a b → (∀ s, z s ∈ Icc a b) → (∀ s, |x - z s| ≤ δ ∧ |y - z s| ≤ δ) → (∀ s, |β s x (z s) - β s y y| < ε) ∧ |sqrt (diagonalWeight S β x) - sqrt (diagonalWeight S β y)| < ε := by -- Take a common radius from coefficient_uniform_continuity and the -- compact uniform continuity of sqrt_mass_regular. The good_cell_diameter -- estimate bounds |x-y| by twice the chosen radius; shrink it once more -- so both the product-metric and scalar distances are strictly inside -- their respective continuity radii. intro ε hε obtain ⟨δc, hδc, hc⟩ := coefficient_uniform_continuity a b S β hcont ε hε have hu := (isCompact_Icc.uniformContinuousOn_of_continuous (sqrt_mass_regular a b hab S hS β hcont hpos).1) obtain ⟨δr, hδr, hr⟩ := (Metric.uniformContinuousOn_iff.mp hu) ε hε let δ : ℝ := min δc δr / 4 have hδ : 0 < δ := by dsimp [δ] positivity have hsmallc : 2 * δ < δc := by dsimp [δ] have := min_le_left δc δr linarith have hsmallr : 2 * δ < δr := by dsimp [δ] have := min_le_right δc δr linarith refine ⟨δ, hδ, ?_⟩ intro x y z hx hy hz hnear have hdiam : |x - y| ≤ 2 * δ := good_cell_diameter S hS z x y δ (fun s => (hnear s).1) (fun s => (hnear s).2) constructor · intro s have hpair : dist (x, z s) (y, y) < δc := by rw [Prod.dist_eq, Real.dist_eq, Real.dist_eq] apply max_lt · exact hdiam.trans_lt hsmallc · have hzy : |z s - y| ≤ δ := by simpa only [abs_sub_comm] using (hnear s).2 linarith exact hc s (x, z s) (y, y) ⟨hx, hz s⟩ ⟨hy, hy⟩ hpair · have hdist : dist x y < δr := by rw [Real.dist_eq] exact hdiam.trans_lt hsmallr simpa only [Real.dist_eq] using hr x hx y hy hdist -
frozen_cell_sqrt_mass_lowertheorem — A frozen nonnegative coefficient family controls the square of the square-root diagonal mass on any measurable part of a cell, provided that the diagonal square root is bounded there by a compatible constant.hypothesesa b :ℝhab :a ≤ bS :ℕβ :Fin S → ℝ → ℝ → ℝB G :Set ℝhB :hG :hsub :B ⊆ Icc a bhGB :G ⊆ Bz :Fin S → ℝγ :Fin S → ℝhγ :∀ s, 0 ≤ γ shβ :∀ x ∈ G, ∀ s, γ s ≤ β s x (z s)hβnonneg :∀ x ∈ B, ∀ s, 0 ≤ β s x (z s)hInt :∀ s, IntegrableOn (fun x => β s x (z s) * |x - z s|) B volumeQ η :ℝhQ :0 ≤ Qhη :0 ≤ η ∧ η < 1hq :∀ x ∈ G, sqrt (diagonalWeight S β x) ≤ Qhcoeff :(1 - η) * Q ^ 2 ≤ ∑ s : Fin S, γ sconclusion(1 - η) * (∫ x in G, sqrt (diagonalWeight S β x)) ^ 2 / 4≤ ∑ s : Fin S, ∫ x in B, β s x (z s) * |x - z s|Proof (Lean source)
theorem frozen_cell_sqrt_mass_lower (a b : ℝ) (hab : a ≤ b) (S : ℕ) (β : Fin S → ℝ → ℝ → ℝ) (B G : Set ℝ) (hB : MeasurableSet B) (hG : MeasurableSet G) (hsub : B ⊆ Icc a b) (hGB : G ⊆ B) (z : Fin S → ℝ) (γ : Fin S → ℝ) (hγ : ∀ s, 0 ≤ γ s) (hβ : ∀ x ∈ G, ∀ s, γ s ≤ β s x (z s)) (hβnonneg : ∀ x ∈ B, ∀ s, 0 ≤ β s x (z s)) (hInt : ∀ s, IntegrableOn (fun x => β s x (z s) * |x - z s|) B volume) (Q η : ℝ) (hQ : 0 ≤ Q) (hη : 0 ≤ η ∧ η < 1) (hq : ∀ x ∈ G, sqrt (diagonalWeight S β x) ≤ Q) (hcoeff : (1 - η) * Q ^ 2 ≤ ∑ s : Fin S, γ s) : (1 - η) * (∫ x in G, sqrt (diagonalWeight S β x)) ^ 2 / 4 ≤ ∑ s : Fin S, ∫ x in B, β s x (z s) * |x - z s| := by -- Bound the square-root integral by Q*volume.real G, square using -- nonnegativity, then apply near_region_moment_lower with γ. have hGsub : G ⊆ Icc a b := hGB.trans hsub have hGfin : volume G < ⊤ := lt_of_le_of_lt (measure_mono hGsub) (measure_Icc_lt_top (μ := volume)) have hnorm : |∫ x in G, sqrt (diagonalWeight S β x)| ≤ Q * volume.real G := by simpa only [Real.norm_eq_abs] using (norm_setIntegral_le_of_norm_le_const (f := fun x : ℝ => sqrt (diagonalWeight S β x)) (s := G) (μ := volume) (C := Q) hGfin (fun x hx => by simpa only [Real.norm_eq_abs, abs_of_nonneg (Real.sqrt_nonneg _)] using hq x hx)) have hvol : 0 ≤ Q * volume.real G := mul_nonneg hQ ENNReal.toReal_nonneg have hsq : (∫ x in G, sqrt (diagonalWeight S β x)) ^ 2 ≤ (Q * volume.real G) ^ 2 := by exact sq_le_sq.mpr (by simpa only [abs_of_nonneg hvol] using hnorm) calc (1 - η) * (∫ x in G, sqrt (diagonalWeight S β x)) ^ 2 / 4 ≤ (1 - η) * (Q * volume.real G) ^ 2 / 4 := by gcongr linarith [hη.2] _ = ((1 - η) * Q ^ 2) * volume.real G ^ 2 / 4 := by ring _ ≤ (∑ s : Fin S, γ s) * volume.real G ^ 2 / 4 := by gcongr _ ≤ ∑ s : Fin S, ∫ x in B, β s x (z s) * |x - z s| := near_region_moment_lower a b hab S β z B G hB hG hsub hGB γ hγ hβ hβnonneg hInt -
good_cell_relative_freezetheorem — A single anchor in a short cell supplies nonnegative frozen coefficients and a common square-root-density bound for every nearby source point, with a uniform relative margin between their squared bound and coefficient sum.hypothesesa b :ℝhab :a < bS :ℕhS :0 < Sβ :Fin S → ℝ → ℝ → ℝhcont :∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2) (Set.Icc a b ×ˢ Set.Icc a b)hpos :∀ s x zifx ∈ Set.Icc a bandz ∈ Set.Icc a bthen0 < β s x zη :ℝ0 < ηη < 1conclusion∃ δ : ℝ,0 < δconclusion 1∃ (γ : Fin S → ℝ) (Q : ℝ),s :0 ≤ γ s0 ≤ Q(1 - η) * Q ^ 2 ≤ ∑ s : Fin S, γ sx ∈ Set.Icc a b :(∀ s, |x - z s| ≤ δ)s :γ s ≤ β s x (z s)sqrt (diagonalWeight S β x) ≤ QProof (Lean source)
theorem good_cell_relative_freeze (a b : ℝ) (hab : a < b) (S : ℕ) (hS : 0 < S) (β : Fin S → ℝ → ℝ → ℝ) (hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2) (Icc a b ×ˢ Icc a b)) (hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z) : ∀ η : ℝ, 0 < η → η < 1 → ∃ δ : ℝ, 0 < δ ∧ ∀ (y : ℝ) (z : Fin S → ℝ), y ∈ Icc a b → (∀ s, z s ∈ Icc a b) → (∀ s, |y - z s| ≤ δ) → ∃ (γ : Fin S → ℝ) (Q : ℝ), (∀ s, 0 ≤ γ s) ∧ 0 ≤ Q ∧ (1 - η) * Q ^ 2 ≤ ∑ s : Fin S, γ s ∧ ∀ x ∈ Icc a b, (∀ s, |x - z s| ≤ δ) → (∀ s, γ s ≤ β s x (z s)) ∧ Real.sqrt (diagonalWeight S β x) ≤ Q := by -- Use coefficient_bounds to obtain a uniform positive minimum c and a -- finite upper bound on the diagonal weight. Choose a uniform continuity -- error e so (1-η)*(sqrt(w(y))+e)^2 ≤ w(y)-S*e for all y in Icc. -- good_cell_uniform_freeze then permits γ_s=β_s(y,y)-e and -- Q=sqrt(w(y))+e, uniformly in x and the reproduction array. classical intro η hη hη1 obtain ⟨c, C, hc, hbounds⟩ := coefficient_bounds a b hab S hS β hcont hpos have hSreal : (0 : ℝ) < S := by exact_mod_cast hS have hC : 0 < C := by have ha : a ∈ Icc a b := ⟨le_refl a, le_of_lt hab⟩ exact lt_of_lt_of_le (lt_of_lt_of_le hc ((hbounds ⟨0, hS⟩ a ha a ha).1)) ((hbounds ⟨0, hS⟩ a ha a ha).2) let R : ℝ := Real.sqrt ((S : ℝ) * C) have hR : 0 ≤ R := Real.sqrt_nonneg _ let D : ℝ := 2 * R + 1 + (S : ℝ) have hD : 0 < D := by dsimp [D]; positivity let e : ℝ := min (c / 2) (min 1 (η * ((S : ℝ) * c) / (2 * D))) have he : 0 < e := by dsimp [e]; positivity have hec : e ≤ c / 2 := min_le_left _ _ have he1 : e ≤ 1 := (min_le_right _ _).trans (min_le_left _ _) have heD : e * D ≤ η * ((S : ℝ) * c) := by have h := min_le_right (c / 2) (min 1 (η * ((S : ℝ) * c) / (2 * D))) have h' := h.trans (min_le_right _ _) dsimp [e] at * have := mul_le_mul_of_nonneg_right h' (by positivity : 0 ≤ 2 * D) rw [div_mul_cancel₀ _ (by positivity : 2 * D ≠ 0)] at this nlinarith obtain ⟨δ, hδ, hfreeze⟩ := good_cell_uniform_freeze a b hab S hS β hcont hpos e he refine ⟨δ, hδ, ?_⟩ intro y z hy hz hyz let w := diagonalWeight S β y let t := Real.sqrt w have hwlow : (S : ℝ) * c ≤ w := by dsimp [w, diagonalWeight] simpa using (Finset.sum_le_sum (s := univ) (fun s hs => (hbounds s y hy y hy).1) : ∑ _s : Fin S, c ≤ ∑ s : Fin S, β s y y) have hwup : w ≤ (S : ℝ) * C := by dsimp [w, diagonalWeight] simpa using (Finset.sum_le_sum (s := univ) (fun s hs => (hbounds s y hy y hy).2) : (∑ s : Fin S, β s y y) ≤ ∑ _s : Fin S, C) have hw0 : 0 ≤ w := le_trans (mul_nonneg (le_of_lt hSreal) (le_of_lt hc)) hwlow have ht0 : 0 ≤ t := Real.sqrt_nonneg _ have ht2 : t ^ 2 = w := Real.sq_sqrt hw0 have htR : t ≤ R := Real.sqrt_le_sqrt hwup have hmargin : (1 - η) * (t + e) ^ 2 ≤ w - (S : ℝ) * e := by have hte : t * e ≤ R * e := mul_le_mul_of_nonneg_right htR (le_of_lt he) have he2 : e ^ 2 ≤ e := by nlinarith have hcross : 0 ≤ 2 * t * e + e ^ 2 := by positivity have hcrossbound : (1 - η) * (2 * t * e + e ^ 2) ≤ 2 * t * e + e ^ 2 := by simpa using mul_le_mul_of_nonneg_right (show 1 - η ≤ 1 by linarith) hcross have hηw : η * ((S : ℝ) * c) ≤ η * w := mul_le_mul_of_nonneg_left hwlow (le_of_lt hη) dsimp [D] at heD nlinarith refine ⟨(fun s => β s y y - e), t + e, ?_, ?_, ?_, ?_⟩ · intro s have := (hbounds s y hy y hy).1 linarith · exact add_nonneg ht0 (le_of_lt he) · have hsum : (∑ s : Fin S, (β s y y - e)) = w - (S : ℝ) * e := by simp [w, diagonalWeight, Finset.sum_sub_distrib] rw [hsum] exact hmargin · intro x hx hxz obtain ⟨hβ, hq⟩ := hfreeze x y z hx hy hz (fun s => ⟨hxz s, hyz s⟩) constructor · intro s have := (abs_lt.mp (hβ s)).1 linarith · dsimp [t] have := (abs_lt.mp hq).2 linarith
LowerLocal 1 core · 2 supporting Local integral estimates for the universal lower bound. ★ near_region_moment_lower
Local integral estimates for the universal lower bound. The cost estimates apply to arbitrary measurable subsets of a cell and the integrability lemma to every subset, without connectedness assumptions.
theorem near_region_moment_lower reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Quantization
For ordered interval endpoints, a finite family of weight functions with one reproduction point per weight, and measurable regions G ⊆ B inside the interval: if nonnegative constants γ bound each weight, evaluated at its reproduction point, from below on G, the weights are nonnegative on B, and each weight times the distance to its reproduction point is integrable on B, then the sum over the family of the integrals over B of weight times distance to the reproduction point is at least the sum of the constants times the squared Lebesgue measure of G, divided by four.
Formal statement
hypotheses
Proof (Lean source)
theorem near_region_moment_lower (a b : ℝ) (hab : a ≤ b)
(S : ℕ) (β : Fin S → ℝ → ℝ → ℝ) (z : Fin S → ℝ)
(B G : Set ℝ) (hB : MeasurableSet B) (hG : MeasurableSet G)
(hsub : B ⊆ Icc a b) (hGB : G ⊆ B)
(γ : Fin S → ℝ) (hγ : ∀ s, 0 ≤ γ s)
(hβ : ∀ x ∈ G, ∀ s, γ s ≤ β s x (z s))
(hβnonneg : ∀ x ∈ B, ∀ s, 0 ≤ β s x (z s))
(hInt : ∀ s, IntegrableOn (fun x => β s x (z s) * |x - z s|) B volume) :
(∑ s : Fin S, γ s) * volume.real G ^ 2 / 4 ≤
∑ s : Fin S, ∫ x in B, β s x (z s) * |x - z s| := by
-- Apply weighted_measurable_cell_moment to G. On G compare the
-- constant-weight integrands with the actual ones; nonnegativity on
-- B permits enlargement of the integration domain from G to B.
have hGsub : G ⊆ Icc a b := hGB.trans hsub
have hdistInt (s : Fin S) : IntegrableOn (fun x => |x - z s|) G volume := by
have hcont : Continuous (fun x : ℝ => |x - z s|) := by fun_prop
exact (hcont.continuousOn.integrableOn_compact isCompact_Icc).mono_set hGsub
have hbound (s : Fin S) :
γ s * (∫ x in G, |x - z s|) ≤
∫ x in B, β s x (z s) * |x - z s| := by
rw [← integral_const_mul]
calc
(∫ x in G, γ s * |x - z s|) ≤
∫ x in G, β s x (z s) * |x - z s| := by
apply setIntegral_mono_on ((hdistInt s).const_mul (γ s))
((hInt s).mono_set hGB) hG
intro x hx
exact mul_le_mul_of_nonneg_right (hβ x hx s) (abs_nonneg _)
_ ≤ ∫ x in B, β s x (z s) * |x - z s| := by
apply setIntegral_mono_set (hInt s)
· filter_upwards [ae_restrict_mem hB] with x hx
exact mul_nonneg (hβnonneg x hx s) (abs_nonneg _)
· exact hGB.eventuallyLE
exact (weighted_measurable_cell_moment a b hab G hG hGsub S γ hγ z).trans
(Finset.sum_le_sum (fun s _ => hbound s))
2 supporting declarations (lemmas, instances)
-
weighted_cell_integrabletheorem — A continuous weighted absolute-distance integrand is integrable on every subset of the compact source interval when its reproduction point also lies in that interval.hypothesesconclusionIntegrableOn (fun x => β x z * |x - z|) B volumeProof (Lean source)
theorem weighted_cell_integrable (a b : ℝ) (β : ℝ → ℝ → ℝ) (hcont : ContinuousOn (fun p : ℝ × ℝ => β p.1 p.2) (Icc a b ×ˢ Icc a b)) (B : Set ℝ) (hsub : B ⊆ Icc a b) (z : ℝ) (hz : z ∈ Icc a b) : IntegrableOn (fun x => β x z * |x - z|) B volume := by have hpair : ContinuousOn (fun x : ℝ => (x, z)) (Icc a b) := by fun_prop have hβ' : ContinuousOn (fun x : ℝ => β x z) (Icc a b) := hcont.comp hpair (fun x hx => ⟨hx, hz⟩) have hdist : ContinuousOn (fun x : ℝ => |x - z|) (Icc a b) := by fun_prop exact (hβ'.mul hdist).integrableOn_compact isCompact_Icc |>.mono_set hsub -
far_region_measure_costtheorem — If all points in a measurable region are at least δ from one of the reproduction points, its paired cost is at least its volume times c*δ, provided every coefficient there is at least c.hypothesesa b :ℝS :ℕβ :Fin S → ℝ → ℝ → ℝz :Fin S → ℝB G :Set ℝhB :hG :hsub :B ⊆ Icc a bhGB :G ⊆ Bc δ :ℝhc :0 ≤ chδ :0 ≤ δhβ :∀ x ∈ G, ∀ s, c ≤ β s x (z s)hβnonneg :∀ x ∈ B, ∀ s, 0 ≤ β s x (z s)hfar :∀ x ∈ G, ∃ s, δ ≤ |x - z s|hInt :∀ s, IntegrableOn (fun x => β s x (z s) * |x - z s|) B volumeconclusionc * δ * volume.real G ≤ ∑ s : Fin S, ∫ x in B, β s x (z s) * |x - z s|Proof (Lean source)
theorem far_region_measure_cost (a b : ℝ) (S : ℕ) (β : Fin S → ℝ → ℝ → ℝ) (z : Fin S → ℝ) (B G : Set ℝ) (hB : MeasurableSet B) (hG : MeasurableSet G) (hsub : B ⊆ Icc a b) (hGB : G ⊆ B) (c δ : ℝ) (hc : 0 ≤ c) (hδ : 0 ≤ δ) (hβ : ∀ x ∈ G, ∀ s, c ≤ β s x (z s)) (hβnonneg : ∀ x ∈ B, ∀ s, 0 ≤ β s x (z s)) (hfar : ∀ x ∈ G, ∃ s, δ ≤ |x - z s|) (hInt : ∀ s, IntegrableOn (fun x => β s x (z s) * |x - z s|) B volume) : c * δ * volume.real G ≤ ∑ s : Fin S, ∫ x in B, β s x (z s) * |x - z s| := by -- Integrate far_point_cost_lower on G. Finite measure follows from -- G ⊆ B ⊆ Icc a b. Compare each nonnegative integrand on G and B, -- then exchange the finite sum and the integral. have hGsub : G ⊆ Icc a b := hGB.trans hsub have hGfin : volume G ≠ ⊤ := (measure_lt_top_of_subset hGsub (measure_Icc_lt_top (μ := volume)).ne).ne have hsumInt : IntegrableOn (fun x => ∑ s : Fin S, β s x (z s) * |x - z s|) G volume := by apply integrable_finsetSum intro s hs exact (hInt s).mono_set hGB have hpoint : ∀ x ∈ G, c * δ ≤ ∑ s : Fin S, β s x (z s) * |x - z s| := by intro x hx exact far_point_cost_lower S β z x c δ hc hδ (hβ x hx) (hfar x hx) calc c * δ * volume.real G = ∫ _x in G, c * δ := by rw [setIntegral_const, smul_eq_mul, mul_comm] _ ≤ ∫ x in G, ∑ s : Fin S, β s x (z s) * |x - z s| := by exact setIntegral_mono_on (integrableOn_const hGfin) hsumInt hG hpoint _ = ∑ s : Fin S, ∫ x in G, β s x (z s) * |x - z s| := by exact integral_finsetSum univ (fun s _ => (hInt s).mono_set hGB) _ ≤ ∑ s : Fin S, ∫ x in B, β s x (z s) * |x - z s| := by apply Finset.sum_le_sum intro s hs apply setIntegral_mono_set (hInt s) · filter_upwards [ae_restrict_mem hB] with x hx exact mul_nonneg (hβnonneg x hx s) (abs_nonneg _) · exact hGB.eventuallyLE
LowerMass 1 core · 0 supporting For a finite measurable partition of [a, b] into cells with reproduction points, each cell splits into its bad region (points at distance at least δ from one of the cell's reproduction points) and the remaining good regi ★ partition_good_mass_identity
Good-region mass of a quantization partition
For a finite measurable partition of [a, b] into cells with reproduction points, each cell splits into its bad region (points at distance at least δ from one of the cell's reproduction points) and the remaining good region. The integral over [a, b] of the square root of the diagonal weight Σ_s β_s(x, x), minus its integral over all bad regions, equals its integral over all good regions, for continuous strictly positive weights β_s. This bookkeeping identity feeds the lower bound on the optimal quantization cost.
Main results
* partition_good_mass_identity — total square-root diagonal mass minus bad-region mass equals
good-region mass, for an arbitrary measurable partition and any threshold δ.
theorem partition_good_mass_identity reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Quantization
On a nondegenerate interval, a nonempty finite weight family with continuous strictly positive weights, and a measurable partition with reproductions and a distance threshold, total square-root mass minus bad-region mass equals good-region mass.
Formal statement
hypotheses
a b :
ℝ
hab :
a < b
S k :
ℕ
hS :
0 < S
β :
Fin S → ℝ → ℝ → ℝ
hcont :
hB :
IsMeasurablePartition a b k B
δ :
ℝ
conclusion
(∫ x in a..b, sqrt (diagonalWeight S β x))
Proof (Lean source)
theorem partition_good_mass_identity (a b : ℝ) (hab : a < b)
(S k : ℕ) (hS : 0 < S) (β : Fin S → ℝ → ℝ → ℝ)
(hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2)
(Icc a b ×ˢ Icc a b))
(hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z)
(B : Fin k → Set ℝ) (z : Fin k → Fin S → ℝ)
(hB : IsMeasurablePartition a b k B) (δ : ℝ) :
(∫ x in a..b, sqrt (diagonalWeight S β x)) -
∑ j : Fin k, ∫ x in badRegion S k δ B z j,
sqrt (diagonalWeight S β x) =
∑ j : Fin k, ∫ x in B j \ badRegion S k δ B z j,
sqrt (diagonalWeight S β x) := by
-- Use integral_iUnion_fintype on the measurable partition, then split
-- each cell into its measurable bad region and complement. The interval
-- integral agrees with the Icc set integral because endpoints are null.
have hsub (j : Fin k) : B j ⊆ Icc a b := by
intro x hx
rw [← hB.2.2]
exact Set.mem_iUnion.mpr ⟨j, hx⟩
have hInt (j : Fin k) :
IntegrableOn (fun x => sqrt (diagonalWeight S β x)) (B j) volume :=
((sqrt_mass_regular a b hab S hS β hcont hpos).1.integrableOn_compact
isCompact_Icc).mono_set (hsub j)
have hsplit (j : Fin k) :
(∫ x in B j \ badRegion S k δ B z j,
sqrt (diagonalWeight S β x)) =
(∫ x in B j, sqrt (diagonalWeight S β x)) -
(∫ x in badRegion S k δ B z j,
sqrt (diagonalWeight S β x)) := by
exact setIntegral_sdiff
(badRegion_measurable S k δ B z hB.1 j) (hInt j)
(by intro x hx; exact hx.1)
have hpartition :
(∫ x in Icc a b, sqrt (diagonalWeight S β x)) =
∑ j : Fin k, ∫ x in B j, sqrt (diagonalWeight S β x) := by
rw [← hB.2.2]
exact integral_iUnion_fintype hB.1 hB.2.1 hInt
rw [intervalIntegral.integral_of_le hab.le, ← integral_Icc_eq_integral_Ioc,
hpartition]
simp_rw [hsplit]
rw [Finset.sum_sub_distrib]
LowerSum 1 core · 0 supporting Sum the sharp local good-cell bound over an arbitrary measurable partition. ★ partition_good_square_sum_lower
Sum the sharp local good-cell bound over an arbitrary measurable partition. The good part of a cell is obtained by removing points far from at least one of its reproduction points.
theorem partition_good_square_sum_lower reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Quantization
On a nondegenerate interval, a nonempty finite weight family with continuous strictly positive weights, every relative error η strictly between zero and one admits a distance threshold δ > 0, the same for all partitions, such that for every positive number of cells, every measurable partition of the interval and every array of reproduction points in the interval, the paired weighted cost is at least (1 − η)/4 times the sum over cells of the squared integral of the square-root diagonal weight over the cell's good part, namely the points of the cell closer than δ to all of that cell's reproduction points.
Formal statement
hypotheses
conclusion
∃ δ : ℝ,
0 < δ
conclusion 1
≤ weightedCost S k β B z
Proof (Lean source)
theorem partition_good_square_sum_lower (a b : ℝ) (hab : a < b)
(S : ℕ) (hS : 0 < S) (β : Fin S → ℝ → ℝ → ℝ)
(hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2)
(Icc a b ×ˢ Icc a b))
(hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z) :
∀ η : ℝ, 0 < η → η < 1 → ∃ δ : ℝ, 0 < δ ∧
∀ k : ℕ, 0 < k →
∀ (B : Fin k → Set ℝ) (z : Fin k → Fin S → ℝ),
IsMeasurablePartition a b k B →
(∀ j s, z j s ∈ Icc a b) →
(1 - η) *
(∑ j : Fin k,
(∫ x in B j \ badRegion S k δ B z j,
sqrt (diagonalWeight S β x)) ^ 2) / 4 ≤
weightedCost S k β B z := by
intro η hη hη1
obtain ⟨δ, hδ, hlocal⟩ :=
good_cell_sqrt_mass_lower a b hab S hS β hcont hpos η hη hη1
refine ⟨δ, hδ, ?_⟩
intro k hk B z hB hz
have hsub (j : Fin k) : B j ⊆ Icc a b := by
intro x hx
rw [← hB.2.2]
exact Set.mem_iUnion.mpr ⟨j, hx⟩
have hcell (j : Fin k) :
(1 - η) *
(∫ x in B j \ badRegion S k δ B z j,
sqrt (diagonalWeight S β x)) ^ 2 / 4 ≤
∑ s : Fin S, ∫ x in B j, β s x (z j s) * |x - z j s| := by
apply hlocal (B j) (B j \ badRegion S k δ B z j) (z j)
(hB.1 j) ((hB.1 j).diff (badRegion_measurable S k δ B z hB.1 j))
(hsub j) (Set.sdiff_subset)
(hz j)
intro x hx s
apply le_of_lt
apply lt_of_not_ge
intro hfar
exact hx.2 ⟨hx.1, ⟨s, hfar⟩⟩
calc
(1 - η) *
(∑ j : Fin k,
(∫ x in B j \ badRegion S k δ B z j,
sqrt (diagonalWeight S β x)) ^ 2) / 4 =
∑ j : Fin k,
(1 - η) *
(∫ x in B j \ badRegion S k δ B z j,
sqrt (diagonalWeight S β x)) ^ 2 / 4 := by
rw [Finset.mul_sum, Finset.sum_div]
_ ≤ ∑ j : Fin k, ∑ s : Fin S,
∫ x in B j, β s x (z j s) * |x - z j s| :=
Finset.sum_le_sum (fun j _ => hcell j)
_ = weightedCost S k β B z := rfl
Main 1 core · 0 supporting The exact high-resolution limit for finite paired weighted scalar L1 quantization on a compact nondegenerate real interval. ★ optimal_scaled_cost_tendsto
The exact high-resolution limit for finite paired weighted scalar L1 quantization on a compact nondegenerate real interval.
theorem optimal_scaled_cost_tendsto reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Quantization
On a nondegenerate interval, a nonempty finite weight family with jointly continuous and strictly positive losses satisfies the high-resolution limit: the number of cells k times the optimal paired L1 cost with k cells converges, as k grows, to one quarter of the squared integral over the interval of the square root of the diagonal weight.
Formal statement
hypotheses
conclusion
Tendsto (fun k : ℕ => (k : ℝ) * optimalCost a b S k β) atTop (nhds ((1 / 4 : ℝ) * (∫ x in a..b, sqrt (diagonalWeight S β x)) ^ 2))
Proof (Lean source)
theorem optimal_scaled_cost_tendsto (a b : ℝ) (hab : a < b)
(S : ℕ) (hS : 0 < S) (β : Fin S → ℝ → ℝ → ℝ)
(hcont : ∀ s, ContinuousOn (fun p : ℝ × ℝ => β s p.1 p.2)
(Icc a b ×ˢ Icc a b))
(hpos : ∀ s x z, x ∈ Icc a b → z ∈ Icc a b → 0 < β s x z) :
Tendsto (fun k : ℕ => (k : ℝ) * optimalCost a b S k β)
atTop (nhds ((1 / 4 : ℝ) *
(∫ x in a..b, sqrt (diagonalWeight S β x)) ^ 2)) := by
-- Squeeze optimalCost between optimal_lower_eventually and the feasible
-- companding cost. The latter has the exact limit by companding_scaled_cost_tendsto.
let A : ℝ := (1 / 4 : ℝ) *
(∫ x in a..b, sqrt (diagonalWeight S β x)) ^ 2
have hcomp := companding_scaled_cost_tendsto a b hab S hS β hcont hpos
apply tendsto_order.2
constructor
· intro c hc
have hε : 0 < (A - c) / 2 := by
exact div_pos (sub_pos.mpr hc) (by norm_num)
obtain ⟨K, hK⟩ :=
optimal_lower_eventually a b hab S hS β hcont hpos ((A - c) / 2) hε
apply Filter.eventually_atTop.2
refine ⟨max K 1, ?_⟩
intro k hk
have hkK : K ≤ k := (le_max_left K 1).trans hk
have hkpos : 0 < k := lt_of_lt_of_le Nat.zero_lt_one ((le_max_right K 1).trans hk)
have hlow := hK k hkK hkpos
dsimp [A] at hε hlow
linarith
· intro c hc
have hevent := (tendsto_order.1 hcomp).2 c hc
have hkEventually : ∀ᶠ k : ℕ in atTop, 0 < k := by
apply Filter.eventually_atTop.2
exact ⟨1, fun k hk => lt_of_lt_of_le Nat.zero_lt_one hk⟩
filter_upwards [hevent, hkEventually] with k hlt hk
obtain ⟨hpart, hmid⟩ :=
companding_feasible a b hab S k hS hk β hcont hpos
have hβ : ∀ s x y, x ∈ Icc a b → y ∈ Icc a b →
0 ≤ β s x y := by
intro s x y hx hy
exact (hpos s x y hx hy).le
have hle := optimalCost_le_feasible a b S k β
(compandingCell a b S k β) (compandingMidpoint a b S k β)
hpart hmid hβ
exact lt_of_le_of_lt
(mul_le_mul_of_nonneg_left hle (Nat.cast_nonneg k)) hlt
Moment 1 core · 4 supporting Absolute-deviation moment inequalities for bounded sets: the tail bound holds for every subset of a bounded interval, the layer-cake and moment bounds for measurable subsets. ★ measurable_cell_moment
Absolute-deviation moment inequalities for bounded sets: the tail bound holds for every subset of a bounded interval, the layer-cake and moment bounds for measurable subsets. These lemmas do not require a cell to be connected.
theorem measurable_cell_moment reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Quantization
For ordered interval endpoints, a reproduction point, and a measurable subset of that interval, absolute-deviation loss is at least one quarter of squared Lebesgue mass.
Formal statement
hypotheses
conclusion
volume.real E ^ 2 / 4 ≤ ∫ x in E, |x - z|
Proof (Lean source)
theorem measurable_cell_moment (a b z : ℝ) (hab : a ≤ b)
(E : Set ℝ) (hE : MeasurableSet E) (hsub : E ⊆ Icc a b) :
volume.real E ^ 2 / 4 ≤ ∫ x in E, |x - z| := by
-- Evaluate the affine left-hand integral in
-- measurable_cell_truncated_layer_cake; it equals volume.real E ^ 2 / 4.
have heval : (∫ r in (0 : ℝ)..volume.real E / 2,
(volume.real E - 2 * r)) = volume.real E ^ 2 / 4 := by
have hmul : (∫ r in (0 : ℝ)..volume.real E / 2, 2 * r) =
2 * (volume.real E / 2) ^ 2 / 2 := by
rw [intervalIntegral.integral_const_mul, integral_id]
ring
rw [intervalIntegral.integral_sub]
· rw [intervalIntegral.integral_const, hmul]
ring
· exact intervalIntegrable_const
· exact (continuous_const.mul continuous_id).intervalIntegrable _ _
rw [← heval]
exact measurable_cell_truncated_layer_cake a b z hab E hE hsub
4 supporting declarations (lemmas, instances)
-
cell_tail_lowertheorem — For a bounded cell, the mass at distance at least r from a point is at least the cell's mass minus the length 2*r of the central band. The cell may be disconnected and need not be measurable, in which case its mass is its Lebesgue outer measure, and the point may lie outside it.hypothesesconclusionvolume.real E ≤ 2 * r + volume.real (E ∩ {x : ℝ | r ≤ |x - z|})Proof (Lean source)
theorem cell_tail_lower (a b z r : ℝ) (hr : 0 ≤ r) (E : Set ℝ) (hsub : E ⊆ Icc a b) : volume.real E ≤ 2 * r + volume.real (E ∩ {x : ℝ | r ≤ |x - z|}) := by -- Split E into the central band and its complement. Bound the band by -- volume (Icc (z-r) (z+r)) = 2*r, including its null endpoints. let C : Set ℝ := Ioo (z - r) (z + r) have hfinite : volume E ≠ ⊤ := by exact (measure_lt_top_of_subset hsub (measure_Icc_lt_top (μ := volume)).ne).ne have hcover : E ⊆ (E ∩ C) ∪ (E ∩ {x : ℝ | r ≤ |x - z|}) := by intro x hx by_cases h : |x - z| < r · left refine ⟨hx, ?_⟩ have h' := (abs_lt.mp h) change z - r < x ∧ x < z + r constructor <;> linarith [h'.1, h'.2] · right exact ⟨hx, le_of_not_gt h⟩ have hcentral : volume.real (E ∩ C) ≤ 2 * r := by calc volume.real (E ∩ C) ≤ volume.real C := measureReal_mono inter_subset_right measure_Ioo_lt_top.ne _ = 2 * r := by dsimp [C] rw [Real.volume_real_Ioo_of_le (by linarith)] ring calc volume.real E ≤ volume.real ((E ∩ C) ∪ (E ∩ {x : ℝ | r ≤ |x - z|})) := measureReal_mono hcover (by finiteness) _ ≤ volume.real (E ∩ C) + volume.real (E ∩ {x : ℝ | r ≤ |x - z|}) := measureReal_union_le _ _ _ ≤ 2 * r + volume.real (E ∩ {x : ℝ | r ≤ |x - z|}) := by linarith -
measurable_cell_truncated_layer_caketheorem — Integrating the distance tails up to half the cell's mass gives a lower bound for the absolute-deviation integral over any bounded measurable cell.hypothesesconclusion(∫ r in (0 : ℝ)..volume.real E / 2, (volume.real E - 2 * r)) ≤ ∫ x in E, |x - z|Proof (Lean source)
theorem measurable_cell_truncated_layer_cake (a b z : ℝ) (hab : a ≤ b) (E : Set ℝ) (hE : MeasurableSet E) (hsub : E ⊆ Icc a b) : (∫ r in (0 : ℝ)..volume.real E / 2, (volume.real E - 2 * r)) ≤ ∫ x in E, |x - z| := by -- Use cell_tail_lower at each nonnegative radius, integrate -- in r, then Tonelli/layer cake to compare truncated tails with distance. let μ : Measure ℝ := volume.restrict E let m := volume.real E let M := |a - z| + |b - z| + (b - a) + 1 have hEfin : volume E ≠ ⊤ := (measure_lt_top_of_subset hsub (measure_Icc_lt_top (μ := volume)).ne).ne have hm : 0 ≤ m := measureReal_nonneg have hmM : m / 2 ≤ M := by have hmass : m ≤ b - a := by calc m ≤ volume.real (Icc a b) := measureReal_mono hsub (measure_Icc_lt_top (μ := volume)).ne _ = b - a := Real.volume_real_Icc_of_le hab dsimp [M] have := abs_nonneg (a - z) have := abs_nonneg (b - z) linarith have hM : 0 ≤ M := by dsimp [M]; positivity have hbound : ∀ x ∈ E, |x - z| ≤ M := by intro x hx have hxa : a ≤ x := (hsub hx).1 have hxb : x ≤ b := (hsub hx).2 have hxle : x - z ≤ M := by have := le_abs_self (b - z) dsimp [M] have := abs_nonneg (a - z) linarith have hxge : -(M) ≤ x - z := by have := neg_le_of_abs_le (le_refl |a - z|) have := neg_abs_le (a - z) dsimp [M] have := abs_nonneg (b - z) linarith exact abs_le.mpr ⟨hxge, hxle⟩ have hfint : Integrable (fun x : ℝ => |x - z|) μ := by change IntegrableOn (fun x : ℝ => |x - z|) E volume exact ((by fun_prop : Continuous (fun x : ℝ => |x - z|)).continuousOn.integrableOn_compact isCompact_Icc).mono_set hsub have hcake := hfint.integral_eq_integral_Ioc_meas_le (μ := μ) (M := M) (Filter.Eventually.of_forall (fun x => abs_nonneg _)) (by filter_upwards [self_mem_ae_restrict hE] with x hx; exact hbound x hx) let T : ℝ → ℝ := fun r => volume.real (E ∩ {x : ℝ | r ≤ |x - z|}) have hanti : Antitone T := by intro s t hst exact measureReal_mono (by intro x hx exact ⟨hx.1, hst.trans hx.2⟩) (measure_ne_top_of_subset inter_subset_left hEfin) have hTmeas : Measurable T := hanti.measurable have hTnonneg (r : ℝ) : 0 ≤ T r := measureReal_nonneg have hTle (r : ℝ) : T r ≤ m := measureReal_mono inter_subset_left hEfin have hTint : IntegrableOn T (Ioc 0 M) volume := by apply Measure.integrableOn_of_bounded measure_Ioc_lt_top.ne hTmeas.aestronglyMeasurable filter_upwards with r rw [Real.norm_eq_abs, abs_of_nonneg (hTnonneg r)] exact hTle r have hcake' : (∫ r in Ioc 0 M, T r) = ∫ x in E, |x - z| := by rw [hcake] congr 1 funext r change T r = (volume.restrict E).real {x : ℝ | r ≤ |x - z|} rw [measureReal_restrict_apply (measurableSet_le measurable_const (by fun_prop))] exact congrArg volume.real (Set.inter_comm _ _) have hlinearInt : IntegrableOn (fun r : ℝ => m - 2 * r) (Ioc 0 (m / 2)) volume := by exact ((by fun_prop : Continuous (fun r : ℝ => m - 2 * r)).continuousOn.integrableOn_compact isCompact_Icc).mono_set Ioc_subset_Icc_self have hTintSmall : IntegrableOn T (Ioc 0 (m / 2)) volume := hTint.mono_set (fun r hr => ⟨hr.1, hr.2.trans hmM⟩) have hpoint : ∀ r ∈ Ioc 0 (m / 2), m - 2 * r ≤ T r := by intro r hr have h := cell_tail_lower a b z r hr.1.le E hsub dsimp [m, T] linarith have hfirst : (∫ r in Ioc 0 (m / 2), m - 2 * r) ≤ (∫ r in Ioc 0 (m / 2), T r) := setIntegral_mono_on hlinearInt hTintSmall measurableSet_Ioc hpoint have hsecond : (∫ r in Ioc 0 (m / 2), T r) ≤ (∫ r in Ioc 0 M, T r) := by apply setIntegral_mono_set hTint · exact Filter.Eventually.of_forall (fun r => hTnonneg r) · exact Filter.Eventually.of_forall (fun r hr => ⟨hr.1, hr.2.trans hmM⟩) rw [intervalIntegral.integral_of_le (by linarith : (0 : ℝ) ≤ m / 2)] exact hfirst.trans (hsecond.trans_eq hcake') -
weighted_measurable_cell_momenttheorem — For a finite family of nonnegative constant weights, separate reproduction points cannot improve the common measurable cell's quarter-square bound.hypothesesProof (Lean source)
theorem weighted_measurable_cell_moment (a b : ℝ) (hab : a ≤ b) (E : Set ℝ) (hE : MeasurableSet E) (hsub : E ⊆ Icc a b) (S : ℕ) (γ : Fin S → ℝ) (hγ : ∀ s, 0 ≤ γ s) (z : Fin S → ℝ) : ((∑ s : Fin S, γ s) * volume.real E ^ 2 / 4) ≤ ∑ s : Fin S, γ s * (∫ x in E, |x - z s|) := by -- Sum measurable_cell_moment after multiplying by each nonnegative γ s. calc ((∑ s : Fin S, γ s) * volume.real E ^ 2 / 4) = ∑ s : Fin S, γ s * (volume.real E ^ 2 / 4) := by rw [← Finset.sum_mul] ring _ ≤ ∑ s : Fin S, γ s * (∫ x in E, |x - z s|) := by apply Finset.sum_le_sum intro s hs exact mul_le_mul_of_nonneg_left (measurable_cell_moment a b (z s) hab E hE hsub) (hγ s) -
interval_midpoint_momenttheorem — The midpoint realizes the exact quarter-square absolute-deviation integral on a nondegenerate or degenerate closed interval.hypothesesa b :ℝhab :a ≤ bconclusion(∫ x in a..b, |x - (a + b) / 2|) = (b - a) ^ 2 / 4Proof (Lean source)
theorem interval_midpoint_moment (a b : ℝ) (hab : a ≤ b) : (∫ x in a..b, |x - (a + b) / 2|) = (b - a) ^ 2 / 4 := by -- Split the interval at its midpoint and integrate the two affine branches. let m := (a + b) / 2 have ham : a ≤ m := by dsimp [m]; linarith have hmb : m ≤ b := by dsimp [m]; linarith have hleft : (∫ x in a..m, |x - m|) = (m - a) ^ 2 / 2 := by have heq : (∫ x in a..m, |x - m|) = ∫ x in a..m, m - x := by apply intervalIntegral.integral_congr intro x hx change |x - m| = m - x rw [abs_of_nonpos (sub_nonpos.mpr ((Set.uIcc_of_le ham ▸ hx).2))] ring rw [heq, intervalIntegral.integral_sub] · simp only [intervalIntegral.integral_const, integral_id] ring · exact intervalIntegrable_const · exact Continuous.intervalIntegrable continuous_id a m have hright : (∫ x in m..b, |x - m|) = (b - m) ^ 2 / 2 := by have heq : (∫ x in m..b, |x - m|) = ∫ x in m..b, x - m := by apply intervalIntegral.integral_congr intro x hx change |x - m| = x - m rw [abs_of_nonneg (sub_nonneg.mpr ((Set.uIcc_of_le hmb ▸ hx).1))] rw [heq, intervalIntegral.integral_sub] · simp only [intervalIntegral.integral_const, integral_id] ring · exact Continuous.intervalIntegrable continuous_id m b · exact intervalIntegrable_const have hc : Continuous (fun x : ℝ => |x - m|) := by fun_prop have hsplit := intervalIntegral.integral_add_adjacent_intervals (hc.intervalIntegrable (μ := volume) a m) (hc.intervalIntegrable (μ := volume) m b) change (∫ x in a..b, |x - m|) = (b - a) ^ 2 / 4 rw [← hsplit, hleft, hright] dsimp [m] ring