Mathlib.Measure­Theory

lemma property_at_of_ae_of_singleton_pos (μ : Measure 𝒳) (p : 𝒳 → Prop) {x : 𝒳} (hp : ∀ᵐ y ∂μ, p y) (hx : μ {x} ≠ 0) : p x := by by_contra hpx have hnull : μ {y | ¬p y} = 0 := by change {y | p y} ∈ ae μ at hp rw [mem_ae_iff] at hp simpa only [Set.compl_setOf] using hp apply hx exact measure_mono_null (by simpa [Set.singleton_subset_iff]) hnull

lemma integrable_of_finite_atomic_support (μ : Measure 𝒳) [IsFiniteMeasure μ] {ι : Type*} [Finite ι] (cell : ι ↪ 𝒳) (hcell : ∀ i, MeasurableSet {cell i}) (hrange : μ (range cell) = μ univ) {E : Type*} [NormedAddCommGroup E] (f : 𝒳 → E) (hf : StronglyMeasurable f) : Integrable f μ := by letI := ofFinite ι rw [measure_eq_fin_sum_smul_dirac_of_range μ cell hcell hrange] apply integrable_finset_sum_measure.2 intro i hi exact (integrable_dirac' hf (by simp)).smul_measure (measure_ne_top μ {cell i})

@[simp] lemma valuesUnionMk_apply_left {M : Type*} [DecidableEq M] {Ω : M → Type*} [∀ n, MeasurableSpace (Ω n)] {A B : Finset M} (a : ValuesOn A Ω) (b : ValuesOn B Ω) {v : M} (hA : v ∈ A) : valuesUnionMk a b ⟨v, mem_union_left B hA⟩ = a ⟨v, hA⟩ := by unfold valuesUnionMk exact dif_pos hA

@[simp] lemma valuesUnionMk_apply_right {M : Type*} [DecidableEq M] {Ω : M → Type*} [∀ n, MeasurableSpace (Ω n)] {A B : Finset M} (a : ValuesOn A Ω) (b : ValuesOn B Ω) {v : M} (hv : v ∈ A ∪ B) (hA : v ∉ A) : valuesUnionMk a b ⟨v, hv⟩ = b ⟨v, (Finset.mem_union.mp hv).resolve_left hA⟩ := by unfold valuesUnionMk exact dif_neg hA

lemma measurable_valuesUnionMk_right {M : Type*} [DecidableEq M] {Ω : M → Type*} [∀ n, MeasurableSpace (Ω n)] {A B : Finset M} (a : ValuesOn A Ω) : Measurable (fun b : ValuesOn B Ω => valuesUnionMk a b) := by refine measurable_pi_iff.mpr ?_ rintro ⟨v, hv⟩ by_cases hA : v ∈ A · have h_eq : (fun b : ValuesOn B Ω => valuesUnionMk a b ⟨v, hv⟩) = (fun _ => a ⟨v, hA⟩) := funext fun _ => valuesUnionMk_apply_left a _ hA rw [h_eq] exact measurable_const · have hB : v ∈ B := (Finset.mem_union.mp hv).resolve_left hA have h_eq : (fun b : ValuesOn B Ω => valuesUnionMk a b ⟨v, hv⟩) = (fun b => b ⟨v, hB⟩) := funext fun _ => valuesUnionMk_apply_right a _ hv hA rw [h_eq] exact measurable_pi_apply _

lemma measurable_valuesUnionMk {M : Type*} [DecidableEq M] {Ω : M → Type*} [∀ n, MeasurableSpace (Ω n)] {A B : Finset M} : Measurable (fun p : ValuesOn A Ω × ValuesOn B Ω => valuesUnionMk p.1 p.2) := by refine measurable_pi_iff.mpr ?_ rintro ⟨v, hv⟩ by_cases hA : v ∈ A · have h_eq : (fun p : ValuesOn A Ω × ValuesOn B Ω => valuesUnionMk p.1 p.2 ⟨v, hv⟩) = (fun p => p.1 ⟨v, hA⟩) := by funext p exact valuesUnionMk_apply_left _ _ hA rw [h_eq] exact (measurable_pi_apply _).comp measurable_fst · have hB : v ∈ B := (Finset.mem_union.mp hv).resolve_left hA have h_eq : (fun p : ValuesOn A Ω × ValuesOn B Ω => valuesUnionMk p.1 p.2 ⟨v, hv⟩) = (fun p => p.2 ⟨v, hB⟩) := by funext p exact valuesUnionMk_apply_right _ _ hv hA rw [h_eq] exact (measurable_pi_apply _).comp measurable_snd

theorem exists_moment_perturbation {T : Finset ℝ} (hT : 3 < T.card) : ∃ δ : ℝ → ℝ, (∑ x ∈ T, δ x = 0) ∧ (∑ x ∈ T, δ x * x = 0) ∧ (∑ x ∈ T, δ x * x ^ 2 = 0) ∧ (∃ x ∈ T, δ x ≠ 0) := by classical set φ : ℝ → (Fin 2 → ℝ) := fun x => ![x, x ^ 2] with hφ have hφinj : Injective φ := by intro x y h; have := congrFun h 0; simpa [hφ] using this have hinjOn : InjOn φ T := hφinj.injOn have hcard : finrank ℝ (Fin 2 → ℝ) + 1 < (T.image φ).card := by rw [Finset.card_image_of_injOn hinjOn, Module.finrank_pi]; simpa using hT obtain ⟨g, hsum0, hgsum, v, hv, hvne⟩ := Module.exists_nontrivial_relation_sum_zero_of_finrank_succ_lt_card hcard rw [Finset.sum_image hinjOn] at hgsum hsum0 have h0 := congrFun hsum0 0 have h1 := congrFun hsum0 1 simp only [Finset.sum_apply, Pi.smul_apply, Pi.zero_apply, smul_eq_mul, hφ, Matrix.cons_val_zero, Matrix.cons_val_one] at h0 h1 obtain ⟨x, hxT, hxne⟩ : ∃ x ∈ T, g (φ x) ≠ 0 := by rw [mem_image] at hv; obtain ⟨x, hxT, rfl⟩ := hv; exact ⟨x, hxT, hvne⟩ exact ⟨fun x => g (φ x), hgsum, h0, h1, x, hxT, hxne⟩

theorem discreteMeasure_apply_compl_of_subset {α : Type*} [MeasurableSpace α] [MeasurableSingletonClass α] {T : Finset α} {w : α → ℝ} {K : Set α} (hTK : ∀ x ∈ T, x ∈ K) : discreteMeasure T w Kᶜ = 0 := by rw [discreteMeasure, Measure.finset_sum_apply] apply Finset.sum_eq_zero intro x hx rw [Measure.smul_apply, Measure.dirac_apply, smul_eq_mul] have : x ∉ Kᶜ := by simp [hTK x hx] simp [this]

theorem isProbabilityMeasure_discreteMeasure {α : Type*} [MeasurableSpace α] {T : Finset α} {w : α → ℝ} (hw : ∀ x ∈ T, 0 ≤ w x) (hsum : ∑ x ∈ T, w x = 1) : IsProbabilityMeasure (discreteMeasure T w) := by constructor rw [discreteMeasure, Measure.finset_sum_apply] have : ∀ x ∈ T, (ofReal (w x) • Measure.dirac x) univ = ofReal (w x) := by intro x hx; rw [Measure.smul_apply, smul_eq_mul]; simp rw [Finset.sum_congr rfl this, ← ENNReal.ofReal_sum_of_nonneg hw, hsum, ENNReal.ofReal_one]

theorem integral_discreteMeasure {α E : Type*} [MeasurableSpace α] [MeasurableSingletonClass α] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {T : Finset α} {w : α → ℝ} (hw : ∀ x ∈ T, 0 ≤ w x) (f : α → E) : ∫ x, f x ∂(discreteMeasure T w) = ∑ x ∈ T, w x • f x := by rw [discreteMeasure, integral_finset_sum_measure] · apply Finset.sum_congr rfl intro x hx rw [integral_smul_measure, integral_dirac, ENNReal.toReal_ofReal (hw x hx)] · intro x hx exact (integrable_dirac enorm_lt_top).smul_measure (by simp)

theorem discreteMeasure_singleton {α : Type*} [MeasurableSpace α] [MeasurableSingletonClass α] {T : Finset α} {w : α → ℝ} {x₀ : α} (hx₀ : x₀ ∈ T) : discreteMeasure T w {x₀} = ofReal (w x₀) := by classical rw [discreteMeasure, Measure.finset_sum_apply] have : ∀ x ∈ T, (ofReal (w x) • Measure.dirac x) {x₀} = if x = x₀ then ofReal (w x) else 0 := by intro x hx rw [Measure.smul_apply, Measure.dirac_apply, smul_eq_mul] by_cases h : x = x₀ <;> simp [h, Set.mem_singleton_iff] rw [Finset.sum_congr rfl this, Finset.sum_ite_eq' T x₀ (fun x => ofReal (w x))] simp [hx₀]

theorem discreteMeasure_midpoint {α : Type*} [MeasurableSpace α] {T : Finset α} {w wp wm : α → ℝ} (hp : ∀ x ∈ T, 0 ≤ wp x) (hm : ∀ x ∈ T, 0 ≤ wm x) (hmid : ∀ x ∈ T, w x = (1 / 2) * wp x + (1 / 2) * wm x) : discreteMeasure T w = (1 / 2 : ℝ≥0∞) • discreteMeasure T wp + (1 / 2 : ℝ≥0∞) • discreteMeasure T wm := by rw [discreteMeasure, discreteMeasure, discreteMeasure, Finset.smul_sum, Finset.smul_sum, ← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro x hx rw [smul_smul, smul_smul, ← add_smul] congr 1 have e2 : (1 / 2 : ℝ≥0∞) = ofReal (1 / 2) := by rw [ENNReal.ofReal_div_of_pos] <;> simp rw [e2, ← ENNReal.ofReal_mul (by norm_num), ← ENNReal.ofReal_mul (by norm_num), ← ENNReal.ofReal_add (mul_nonneg (by norm_num) (hp x hx)) (mul_nonneg (by norm_num) (hm x hx)), ← hmid x hx]

theorem exists_isMinOn_momentSlice {Ω : Type*} [MeasurableSpace Ω] [TopologicalSpace Ω] [T2Space Ω] [BorelSpace Ω] [CompactSpace Ω] (g₁ g₂ f : Ω →ᵇ ℝ) (c₁ c₂ : ℝ) (hne : {μ : ProbabilityMeasure Ω | ∫ x, g₁ x ∂μ = c₁ ∧ ∫ x, g₂ x ∂μ = c₂}.Nonempty) : ∃ μ ∈ {μ : ProbabilityMeasure Ω | ∫ x, g₁ x ∂μ = c₁ ∧ ∫ x, g₂ x ∂μ = c₂}, ∀ ν ∈ {μ : ProbabilityMeasure Ω | ∫ x, g₁ x ∂μ = c₁ ∧ ∫ x, g₂ x ∂μ = c₂}, ∫ x, f x ∂(μ : Measure Ω) ≤ ∫ x, f x ∂(ν : Measure Ω) := by set C := {μ : ProbabilityMeasure Ω | ∫ x, g₁ x ∂μ = c₁ ∧ ∫ x, g₂ x ∂μ = c₂} with hC have hcont1 : Continuous fun μ : ProbabilityMeasure Ω => ∫ x, g₁ x ∂μ := ProbabilityMeasure.continuous_integral_boundedContinuousFunction g₁ have hcont2 : Continuous fun μ : ProbabilityMeasure Ω => ∫ x, g₂ x ∂μ := ProbabilityMeasure.continuous_integral_boundedContinuousFunction g₂ have hcontf : Continuous fun μ : ProbabilityMeasure Ω => ∫ x, f x ∂μ := ProbabilityMeasure.continuous_integral_boundedContinuousFunction f have hCclosed : IsClosed C := by have : C = (fun μ : ProbabilityMeasure Ω => ∫ x, g₁ x ∂μ) ⁻¹' {c₁} ∩ (fun μ : ProbabilityMeasure Ω => ∫ x, g₂ x ∂μ) ⁻¹' {c₂} := rfl rw [this] exact (isClosed_singleton.preimage hcont1).inter (isClosed_singleton.preimage hcont2) have hCcompact : IsCompact C := hCclosed.isCompact obtain ⟨μ, hμC, hmin⟩ := hCcompact.exists_isMinOn hne hcontf.continuousOn exact ⟨μ, hμC, fun ν hν => hmin hν⟩

theorem not_four_distinct_in_support {a b s : ℝ} {μ : Measure ℝ} (hext : IsExtremePoint (MomentSlice a b s) μ) (x : Fin 4 → ℝ) (hinj : Injective x) (hsupp : ∀ i, x i ∈ μ.support) : False := by classical obtain ⟨hprob, hcompl, hmean, hsec⟩ := hext.1 -- (a) integrability of `id` and `t^2` against the probability measure `μ`. have hbdd : ∀ᵐ t ∂μ, t ∈ Icc a b := by rw [ae_iff]; exact hcompl set C : ℝ := max |a| |b| with hC_def have hCnn : 0 ≤ C := le_trans (abs_nonneg a) (le_max_left _ _) have hbound1 : ∀ᵐ t ∂μ, ‖(fun t => t) t‖ ≤ (fun _ => C) t := by filter_upwards [hbdd] with t ht obtain ⟨hat, htb⟩ := ht simp only [Real.norm_eq_abs] rw [abs_le] refine ⟨?_, ?_⟩ · have h1 : -|a| ≤ a := neg_abs_le a have h2 : |a| ≤ C := le_max_left _ _ linarith · have h1 : b ≤ |b| := le_abs_self b have h2 : |b| ≤ C := le_max_right _ _ linarith have hint1 : Integrable (fun t => t) μ := (integrable_const C).mono' (by fun_prop) hbound1 have hbound2 : ∀ᵐ t ∂μ, ‖(fun t => t ^ 2) t‖ ≤ (fun _ => C ^ 2) t := by filter_upwards [hbound1] with t ht simp only [Real.norm_eq_abs] at ht ⊢ rw [abs_pow] nlinarith [abs_nonneg t, ht, hCnn] have hint2 : Integrable (fun t => t ^ 2) μ := (integrable_const (C ^ 2)).mono' (by fun_prop) hbound2 -- (b) four pairwise-disjoint open balls around the support points. have hdist_pos : ∀ i j, i ≠ j → 0 < dist (x i) (x j) := fun i j hij => dist_pos.mpr (fun h => hij (hinj h)) set r : ℝ := (Finset.univ.inf' Finset.univ_nonempty (fun p : Fin 4 × Fin 4 => if p.1 = p.2 then (1 : ℝ) else dist (x p.1) (x p.2))) / 2 with hr_def have hr_pos : 0 < r := by have hpos : 0 < Finset.univ.inf' Finset.univ_nonempty (fun p : Fin 4 × Fin 4 => if p.1 = p.2 then (1 : ℝ) else dist (x p.1) (x p.2)) := by rw [Finset.lt_inf'_iff] intro p _ by_cases hp : p.1 = p.2 · simp [hp] · simp only [hp, if_false]; exact hdist_pos p.1 p.2 hp rw [hr_def]; linarith have hr_le : ∀ i j, i ≠ j → 2 * r ≤ dist (x i) (x j) := by intro i j hij have hle := Finset.inf'_le (fun p : Fin 4 × Fin 4 => if p.1 = p.2 then (1 : ℝ) else dist (x p.1) (x p.2)) (Finset.mem_univ (i, j)) simp only [hij, if_false] at hle rw [hr_def]; linarith set U : Fin 4 → Set ℝ := fun i => ball (x i) r with hU_def have hUopen : ∀ i, IsOpen (U i) := fun i => Metric.isOpen_ball have hxU : ∀ i, x i ∈ U i := fun i => Metric.mem_ball_self hr_pos have hUdisj : Pairwise (onFun Disjoint U) := by intro i j hij refine Metric.ball_disjoint_ball ?_ have := hr_le i j hij; linarith have hUmeas : ∀ i, MeasurableSet (U i) := fun i => (hUopen i).measurableSet have hUpos : ∀ i, 0 < μ (U i) := fun i => (Measure.mem_support_iff_forall (x i)).1 (hsupp i) (U i) ((hUopen i).mem_nhds (hxU i)) have hUne : ∀ i, μ (U i) ≠ ∞ := fun i => measure_ne_top μ (U i) -- (d)–(e) linear dependence of the four restriction moment vectors in ℝ³. set v : Fin 4 → (Fin 3 → ℝ) := fun i => ![(μ (U i)).toReal, ∫ t in U i, t ∂μ, ∫ t in U i, t ^ 2 ∂μ] with hv_def have hdep : ¬ LinearIndependent ℝ v := by intro hli have hcard := hli.fintype_card_le_finrank simp only [Fintype.card_fin, Module.finrank_pi] at hcard omega rw [Fintype.not_linearIndependent_iff] at hdep obtain ⟨g, hgsum, i₀, hi₀⟩ := hdep have H0 : ∑ i, g i * (μ (U i)).toReal = 0 := by have h := congrFun hgsum 0 simpa [Finset.sum_apply, Pi.smul_apply, hv_def, smul_eq_mul] using h have H1 : ∑ i, g i * (∫ t in U i, t ∂μ) = 0 := by have h := congrFun hgsum 1 simpa [Finset.sum_apply, Pi.smul_apply, hv_def, smul_eq_mul] using h have H2 : ∑ i, g i * (∫ t in U i, t ^ 2 ∂μ) = 0 := by have h := congrFun hgsum 2 simpa [Finset.sum_apply, Pi.smul_apply, hv_def, smul_eq_mul] using h -- (f) small step size keeping all perturbed weights nonnegative. set Mg : ℝ := Finset.univ.sup' Finset.univ_nonempty (fun i => |g i|) with hMg_def have hMgnn : 0 ≤ Mg := le_trans (abs_nonneg (g i₀)) (Finset.le_sup' (fun i => |g i|) (Finset.mem_univ i₀)) set ε : ℝ := 1 / (2 * (1 + Mg)) with hε_def have hden : 0 < 2 * (1 + Mg) := by positivity have hε_pos : 0 < ε := by rw [hε_def]; positivity have hε_bound : ∀ i, ε * |g i| ≤ 1 / 2 := by intro i have hgi : |g i| ≤ Mg := Finset.le_sup' (fun i => |g i|) (Finset.mem_univ i) have heq : ε * |g i| = |g i| / (2 * (1 + Mg)) := by rw [hε_def]; ring rw [heq, div_le_iff₀ hden]; nlinarith have hcoef_pos : ∀ (σ : ℝ), |σ| ≤ 1 → ∀ i, 0 ≤ 1 + σ * ε * g i := by intro σ hσ i have h1 : |σ * ε * g i| ≤ 1 / 2 := by have heq : |σ * ε * g i| = |σ| * (ε * |g i|) := by rw [abs_mul, abs_mul, abs_of_pos hε_pos]; ring rw [heq] calc |σ| * (ε * |g i|) ≤ 1 * (1 / 2) := mul_le_mul hσ (hε_bound i) (by positivity) (by norm_num) _ = 1 / 2 := by norm_num have := (abs_le.mp h1).1; linarith -- (g) measure decomposition over the disjoint cover. set W : Set ℝ := ⋃ i, U i with hW_def have hWmeas : MeasurableSet W := MeasurableSet.iUnion hUmeas have hrestrictW : μ.restrict W = ∑ i, μ.restrict (U i) := by rw [hW_def, Measure.restrict_iUnion hUdisj hUmeas, Measure.sum_fintype] have hdecomp : μ = μ.restrict Wᶜ + ∑ i, μ.restrict (U i) := by rw [← hrestrictW, add_comm] exact (Measure.restrict_add_restrict_compl hWmeas).symm -- (h) the two perturbed measures. set pert : ℝ → Measure ℝ := fun σ => μ.restrict Wᶜ + ∑ i, ofReal (1 + σ * ε * g i) • μ.restrict (U i) with hpert_def have hpert_integral : ∀ (σ : ℝ), |σ| ≤ 1 → ∀ (f : ℝ → ℝ), Integrable f μ → ∫ t, f t ∂(pert σ) = (∫ t in Wᶜ, f t ∂μ) + ∑ i, (1 + σ * ε * g i) * (∫ t in U i, f t ∂μ) := by intro σ hσ f hf have hsum_int : Integrable f (∑ i, ofReal (1 + σ * ε * g i) • μ.restrict (U i)) := (integrable_finset_sum_measure).2 (fun i _ => (hf.restrict).smul_measure ENNReal.ofReal_ne_top) rw [hpert_def, integral_add_measure hf.restrict hsum_int, integral_finset_sum_measure (fun i _ => (hf.restrict).smul_measure ENNReal.ofReal_ne_top)] congr 1 apply Finset.sum_congr rfl intro i _ rw [integral_smul_measure, ENNReal.toReal_ofReal (hcoef_pos σ hσ i), smul_eq_mul] have hsplit : ∀ (f : ℝ → ℝ), Integrable f μ → (∫ t in Wᶜ, f t ∂μ) + ∑ i, (∫ t in U i, f t ∂μ) = ∫ t, f t ∂μ := by intro f hf conv_rhs => rw [hdecomp] rw [integral_add_measure hf.restrict ((integrable_finset_sum_measure).2 (fun i _ => hf.restrict)), integral_finset_sum_measure (fun i _ => hf.restrict)] have hmass1 : (μ Wᶜ).toReal + ∑ i, (μ (U i)).toReal = 1 := by have hsplit1 := hsplit (fun _ => (1 : ℝ)) (integrable_const 1) simpa [setIntegral_const, integral_const, hprob.measure_univ, measureReal_def] using hsplit1 have hpert_mem : ∀ (σ : ℝ), |σ| ≤ 1 → pert σ ∈ MomentSlice a b s := by intro σ hσ have hmean' : ∫ t, t ∂(pert σ) = 0 := by rw [hpert_integral σ hσ (fun t => t) hint1] have hcollect : (∫ t in Wᶜ, t ∂μ) + ∑ i, (1 + σ * ε * g i) * (∫ t in U i, t ∂μ) = ((∫ t in Wᶜ, t ∂μ) + ∑ i, (∫ t in U i, t ∂μ)) + σ * ε * ∑ i, g i * (∫ t in U i, t ∂μ) := by rw [add_assoc] congr 1 rw [Finset.mul_sum, ← Finset.sum_add_distrib] apply Finset.sum_congr rfl; intro i _; ring rw [hcollect, hsplit (fun t => t) hint1, hmean, H1]; ring have hsec' : ∫ t, t ^ 2 ∂(pert σ) = s := by rw [hpert_integral σ hσ (fun t => t ^ 2) hint2] have hcollect : (∫ t in Wᶜ, t ^ 2 ∂μ) + ∑ i, (1 + σ * ε * g i) * (∫ t in U i, t ^ 2 ∂μ) = ((∫ t in Wᶜ, t ^ 2 ∂μ) + ∑ i, (∫ t in U i, t ^ 2 ∂μ)) + σ * ε * ∑ i, g i * (∫ t in U i, t ^ 2 ∂μ) := by rw [add_assoc] congr 1 rw [Finset.mul_sum, ← Finset.sum_add_distrib] apply Finset.sum_congr rfl; intro i _; ring rw [hcollect, hsplit (fun t => t ^ 2) hint2, hsec, H2]; ring have hsupp' : (pert σ) (Icc a b)ᶜ = 0 := by rw [hpert_def] simp only [Measure.add_apply, Measure.finset_sum_apply, Measure.smul_apply, smul_eq_mul] have hWc : μ.restrict Wᶜ (Icc a b)ᶜ = 0 := by rw [Measure.restrict_apply measurableSet_Icc.compl] exact le_antisymm (le_trans (measure_mono Set.inter_subset_left) (le_of_eq hcompl)) zero_le have hUc : ∀ i, μ.restrict (U i) (Icc a b)ᶜ = 0 := by intro i rw [Measure.restrict_apply measurableSet_Icc.compl] exact le_antisymm (le_trans (measure_mono Set.inter_subset_left) (le_of_eq hcompl)) zero_le rw [hWc, zero_add] apply Finset.sum_eq_zero intro i _ rw [hUc i, mul_zero] have hprob' : IsProbabilityMeasure (pert σ) := by refine ⟨?_⟩ rw [hpert_def] simp only [Measure.add_apply, Measure.finset_sum_apply, Measure.smul_apply, smul_eq_mul, Measure.restrict_apply_univ] have hreg : ∀ i, (1 + σ * ε * g i) * (μ (U i)).toReal = (μ (U i)).toReal + (σ * ε) * (g i * (μ (U i)).toReal) := by intro i; ring have hreal : (μ Wᶜ).toReal + ∑ i, (1 + σ * ε * g i) * (μ (U i)).toReal = 1 := by rw [Finset.sum_congr rfl (fun i _ => hreg i), Finset.sum_add_distrib, ← Finset.mul_sum, H0, mul_zero, add_zero] exact hmass1 have hWfin : μ Wᶜ ≠ ∞ := measure_ne_top μ _ have hnn : (0 : ℝ) ≤ ∑ i, (1 + σ * ε * g i) * (μ (U i)).toReal := sum_nonneg (fun i _ => mul_nonneg (hcoef_pos σ hσ i) ENNReal.toReal_nonneg) calc μ Wᶜ + ∑ i, ofReal (1 + σ * ε * g i) * μ (U i) = ofReal ((μ Wᶜ).toReal + ∑ i, (1 + σ * ε * g i) * (μ (U i)).toReal) := by rw [ENNReal.ofReal_add ENNReal.toReal_nonneg hnn, ENNReal.ofReal_toReal hWfin] congr 1 rw [ENNReal.ofReal_sum_of_nonneg (fun i _ => mul_nonneg (hcoef_pos σ hσ i) ENNReal.toReal_nonneg)] apply Finset.sum_congr rfl intro i _ rw [ENNReal.ofReal_mul (hcoef_pos σ hσ i), ENNReal.ofReal_toReal (hUne i)] _ = ofReal 1 := by rw [hreal] _ = 1 := by simp exact ⟨hprob', hsupp', hmean', hsec'⟩ -- (j) the two perturbations are distinct, witnessed on `U i₀`. have hval : ∀ (σ : ℝ), (pert σ) (U i₀) = ofReal (1 + σ * ε * g i₀) * μ (U i₀) := by intro σ rw [hpert_def] simp only [Measure.add_apply, Measure.finset_sum_apply, Measure.smul_apply, smul_eq_mul] have hsubW : U i₀ ⊆ W := fun y hy => Set.mem_iUnion.2 ⟨i₀, hy⟩ have hWc0 : μ.restrict Wᶜ (U i₀) = 0 := by rw [Measure.restrict_apply (hUmeas i₀)] rw [(disjoint_compl_right.mono_left hsubW).inter_eq, measure_empty] have hUi : ∀ j, μ.restrict (U j) (U i₀) = if j = i₀ then μ (U i₀) else 0 := by intro j rw [Measure.restrict_apply (hUmeas i₀)] by_cases hji : j = i₀ · subst hji; rw [Set.inter_self]; simp · have hdis : Disjoint (U i₀) (U j) := hUdisj (fun h => hji h.symm) rw [hdis.inter_eq, measure_empty]; simp [hji] rw [hWc0, zero_add, Finset.sum_eq_single i₀ (fun j _ hj => by rw [hUi j]; simp [hj]) (fun h => absurd (Finset.mem_univ i₀) h)] rw [hUi i₀]; simp have hdistinct : pert 1 ≠ pert (-1) := by intro heq have e1 := hval 1 have e2 := hval (-1) rw [heq] at e1 rw [e1] at e2 -- e2 : ofReal (1+1εg i₀) * μ (U i₀) = ofReal (1+(-1)εg i₀) * μ (U i₀) have hreal := congrArg toReal e2 rw [ENNReal.toReal_mul, ENNReal.toReal_mul, ENNReal.toReal_ofReal (hcoef_pos 1 (by norm_num) i₀), ENNReal.toReal_ofReal (hcoef_pos (-1) (by norm_num) i₀)] at hreal have hpos : 0 < (μ (U i₀)).toReal := ENNReal.toReal_pos (hUpos i₀).ne' (hUne i₀) have hz : ε * g i₀ = 0 := by have h2 : (ε * g i₀) * (μ (U i₀)).toReal = 0 := by linear_combination hreal / 2 -- … truncated; follow the source link for the rest …

theorem support_finite_ncard_le_three_of_isExtremePoint {a b s : ℝ} {μ : Measure ℝ} (hext : IsExtremePoint (MomentSlice a b s) μ) : μ.support.Finite ∧ μ.support.ncard ≤ 3 := by classical let S : Set ℝ := μ.support have hno : ∀ (y : Fin 4 → ℝ), Injective y → (∀ i, y i ∈ S) → False := by intro y hyinj hysupp exact not_four_distinct_in_support hext y hyinj hysupp constructor · by_contra hinf have hInf : S.Infinite := by simpa [S, Set.not_finite] using hinf obtain ⟨t, hts, htfin, htc⟩ := hInf.exists_subset_ncard_eq 4 have hcard : htfin.toFinset.card = 4 := by simpa [Set.ncard_eq_toFinset_card t htfin] using htc let e : Fin 4 ↪o ℝ := htfin.toFinset.orderEmbOfFin hcard exact hno (fun i => e i) e.injective (fun i => by have hmemFin : e i ∈ htfin.toFinset := by change htfin.toFinset.orderEmbOfFin hcard i ∈ htfin.toFinset exact Finset.orderEmbOfFin_mem htfin.toFinset hcard i exact hts (by simpa [Set.Finite.mem_toFinset] using hmemFin)) · by_contra hle push_neg at hle have h4 : 4 ≤ S.ncard := Nat.succ_le_of_lt hle obtain ⟨t, hts, htc⟩ := Set.exists_subset_card_eq (s := S) h4 have htfin : t.Finite := Set.finite_of_ncard_ne_zero (by rw [htc]; simp) have hcard : htfin.toFinset.card = 4 := by simpa [Set.ncard_eq_toFinset_card t htfin] using htc let e : Fin 4 ↪o ℝ := htfin.toFinset.orderEmbOfFin hcard exact hno (fun i => e i) e.injective (fun i => by have hmemFin : e i ∈ htfin.toFinset := by change htfin.toFinset.orderEmbOfFin hcard i ∈ htfin.toFinset exact Finset.orderEmbOfFin_mem htfin.toFinset hcard i exact hts (by simpa [Set.Finite.mem_toFinset] using hmemFin))

theorem isAtomic_le_three_of_isExtremePoint {a b s : ℝ} {μ : Measure ℝ} (hext : IsExtremePoint (MomentSlice a b s) μ) : ∃ (T : Finset ℝ) (w : ℝ → ℝ), (∀ x ∈ T, 0 < w x) ∧ (∀ x ∈ T, x ∈ Icc a b) ∧ T.card ≤ 3 ∧ μ = discreteMeasure T w := by classical obtain ⟨hprob, hcompl, _, _⟩ := hext.1 obtain ⟨hsuppfin, hsuppcard⟩ := support_finite_ncard_le_three_of_isExtremePoint hext let T : Finset ℝ := hsuppfin.toFinset let w : ℝ → ℝ := fun x => (μ {x}).toReal have hTsupport : (T : Set ℝ) = μ.support := by simp [T] have hTcard : T.card ≤ 3 := by have hcard : T.card = μ.support.ncard := by simp [T, Set.ncard_eq_toFinset_card μ.support hsuppfin] omega have hsingle_pos : ∀ x ∈ μ.support, 0 < μ {x} := by intro x hx let V : Set ℝ := (μ.support \ {x})ᶜ have hVopen : IsOpen V := (hsuppfin.diff (t := ({x} : Set ℝ))).isClosed.isOpen_compl have hxV : x ∈ V := by simp [V] have hVpos : 0 < μ V := (Measure.mem_support_iff_forall x).1 hx V (hVopen.mem_nhds hxV) have hVS : V ∩ μ.support = {x} := by ext y by_cases hyx : y = x · subst hyx simp [V, hx] · simp [V, hyx] have hconull : μ μ.supportᶜ = 0 := Measure.measure_compl_support have hVeq : μ (V ∩ μ.support) = μ V := measure_inter_conull (μ := μ) (s := V) hconull rw [hVS] at hVeq rwa [hVeq] have hpos : ∀ x ∈ T, 0 < w x := by intro x hxT have hxS : x ∈ μ.support := hTsupport ▸ Finset.mem_coe.mpr hxT have hlt : μ {x} ≠ ∞ := by have hle : μ {x} ≤ μ univ := measure_mono (Set.subset_univ _) rw [hprob.measure_univ] at hle exact ne_top_of_le_ne_top ENNReal.one_ne_top hle have hxpos := hsingle_pos x hxS simpa only [w] using ENNReal.toReal_pos hxpos.ne' hlt have hTab : ∀ x ∈ T, x ∈ Icc a b := by intro x hxT by_contra hxnot have hxS : x ∈ μ.support := hTsupport ▸ Finset.mem_coe.mpr hxT have hxpos : 0 < μ {x} := hsingle_pos x hxS have hsub : ({x} : Set ℝ) ⊆ (Icc a b)ᶜ := by simpa [Set.subset_def] using hxnot have hle : μ {x} ≤ μ (Icc a b)ᶜ := measure_mono hsub rw [hcompl] at hle exact (ne_of_gt hxpos) (le_antisymm hle zero_le) refine ⟨T, w, hpos, hTab, hTcard, ?_⟩ refine Measure.ext fun A hA => ?_ have hconull : μ μ.supportᶜ = 0 := Measure.measure_compl_support have hAinter : μ (A ∩ μ.support) = μ A := measure_inter_conull (μ := μ) (s := A) hconull rw [← hAinter] have hUnion : A ∩ μ.support = ⋃ x ∈ T.filter (fun x => x ∈ A), ({x} : Set ℝ) := by ext y simp [T, Set.Finite.mem_toFinset, and_left_comm, and_assoc] rw [hUnion] rw [measure_biUnion_finset] · rw [discreteMeasure, Measure.finset_sum_apply, Finset.sum_filter] apply Finset.sum_congr rfl intro x hx rw [Measure.smul_apply, Measure.dirac_apply, smul_eq_mul] have hlt : μ {x} ≠ ∞ := by have hle : μ {x} ≤ μ univ := measure_mono (Set.subset_univ _) rw [hprob.measure_univ] at hle exact ne_top_of_le_ne_top ENNReal.one_ne_top hle by_cases hxA : x ∈ A · simp [hxA, w, ENNReal.ofReal_toReal hlt] · simp [hxA] · intro x _ y _ hxy exact Set.disjoint_singleton.2 hxy · intro x _ exact MeasurableSet.singleton x

theorem exists_cardSupportLe_three_of_isExtremePoint {a b s : ℝ} {μ : Measure ℝ} (hext : IsExtremePoint (MomentSlice a b s) μ) : ∃ T : Finset ℝ, T.card ≤ 3 ∧ μ (↑T : Set ℝ)ᶜ = 0 := by classical obtain ⟨hsuppfin, hsuppcard⟩ := support_finite_ncard_le_three_of_isExtremePoint hext refine ⟨hsuppfin.toFinset, ?_, ?_⟩ · simpa [Set.ncard_eq_toFinset_card μ.support hsuppfin] using hsuppcard · rw [Set.Finite.coe_toFinset]; exact Measure.measure_compl_support

theorem integral_cellConst {ι : Type*} [Fintype ι] [IsFiniteMeasure μ] {H : Ω → ι} (hfiber : ∀ h, MeasurableSet (H ⁻¹' {h})) (c : ι → ℝ) : ∫ ω, c (H ω) ∂μ = ∑ h : ι, c h * (μ (H ⁻¹' {h})).toReal := by have h := integral_cellConst_mul hfiber c (f := fun _ => (1 : ℝ)) (hf := (integrable_const (1 : ℝ) : Integrable (fun _ : Ω => (1 : ℝ)) μ)) simpa [mul_one, setIntegral_const, smul_eq_mul, measureReal_def] using h

lemma compProd_eq_prod_withDensity_fiber (μ : Measure α) (ρ : Measure β) (κ : Kernel α β) [SFinite μ] [SigmaFinite ρ] [IsSFiniteKernel κ] (hfiber : ∀ᵐ a ∂μ, κ a ≪ ρ) (hmeas : AEMeasurable (fun p : α × β => (κ p.1).rnDeriv ρ p.2) (μ.prod ρ)) : μ ⊗ₘ κ = (μ.prod ρ).withDensity (fun p : α × β => (κ p.1).rnDeriv ρ p.2) := by ext s hs rw [Measure.compProd_apply hs, withDensity_apply _ hs] rw [← lintegral_indicator hs] rw [lintegral_prod] · refine lintegral_congr_ae ?_ filter_upwards [hfiber] with a ha have hsec : MeasurableSet (Prod.mk a ⁻¹' s) := measurable_prodMk_left hs change (κ a) (Prod.mk a ⁻¹' s) = ∫⁻ y, (Prod.mk a ⁻¹' s).indicator (fun y => (κ a).rnDeriv ρ y) y ∂ρ rw [lintegral_indicator hsec] rw [← Measure.setLIntegral_rnDeriv ha (Prod.mk a ⁻¹' s)] · exact hmeas.indicator hs

lemma abs_le_one_ae_of_setIntegral_le_measure {Ω : Type*} [MeasurableSpace Ω] (mu : Measure Ω) [IsFiniteMeasure mu] (f : Ω → ℝ) (hf : Measurable f) (hdom : ∀ A, MeasurableSet A → |∫ x in A, f x ∂mu| ≤ (mu A).toReal) : ∀ᵐ x ∂mu, |f x| ≤ 1 := by have hupper : ∀ q : ℝ, 1 < q → ∀ᵐ x ∂mu, f x ≤ q := by intro q hq have hslice : ∀ m : ℕ, ∀ᵐ x ∂mu, ¬(q < f x ∧ f x ≤ (m : ℝ)) := by intro m let A : Set Ω := {x | q < f x ∧ f x ≤ (m : ℝ)} have hA : MeasurableSet A := (measurableSet_Ioi.preimage hf).inter (measurableSet_Iic.preimage hf) have hfin : mu A < ∞ := measure_lt_top mu A have hfA : IntegrableOn f A mu := by apply IntegrableOn.of_bound hfin hf.aestronglyMeasurable.restrict (m : ℝ) filter_upwards [self_mem_ae_restrict hA] with x hxA rw [Real.norm_eq_abs, abs_of_pos (lt_trans (by linarith) hxA.1)] exact hxA.2 have hconst : IntegrableOn (fun _ : Ω => q) A mu := integrableOn_const hfin.ne have hlower : q * (mu A).toReal ≤ ∫ x in A, f x ∂mu := by calc q * (mu A).toReal = ∫ _ in A, q ∂mu := by rw [setIntegral_const] simp [Measure.real] ring _ ≤ ∫ x in A, f x ∂mu := integral_mono_ae hconst hfA (ae_restrict_iff' hA |>.2 <| by filter_upwards with x hx exact hx.1.le) have hupperInt : (∫ x in A, f x ∂mu) ≤ (mu A).toReal := (le_abs_self _).trans (hdom A hA) have hzeroReal : (mu A).toReal = 0 := by have hnonneg : 0 ≤ (mu A).toReal := ENNReal.toReal_nonneg nlinarith have hzero : mu A = 0 := by rw [ENNReal.toReal_eq_zero_iff] at hzeroReal exact hzeroReal.resolve_right hfin.ne rw [ae_iff] simpa [A] using hzero rw [← ae_all_iff] at hslice filter_upwards [hslice] with x hx by_contra hqx have hqfx : q < f x := lt_of_not_ge hqx obtain ⟨m, hm⟩ := exists_nat_ge (f x) exact hx m ⟨hqfx, hm⟩ have hlower : ∀ q : ℝ, 1 < q → ∀ᵐ x ∂mu, -q ≤ f x := by intro q hq have hslice : ∀ m : ℕ, ∀ᵐ x ∂mu, ¬(-(m : ℝ) ≤ f x ∧ f x < -q) := by intro m let A : Set Ω := {x | -(m : ℝ) ≤ f x ∧ f x < -q} have hA : MeasurableSet A := (measurableSet_Ici.preimage hf).inter (measurableSet_Iio.preimage hf) have hfin : mu A < ∞ := measure_lt_top mu A have hfA : IntegrableOn f A mu := by apply IntegrableOn.of_bound hfin hf.aestronglyMeasurable.restrict (m : ℝ) filter_upwards [self_mem_ae_restrict hA] with x hxA rw [Real.norm_eq_abs, abs_of_neg (lt_trans hxA.2 (neg_lt_zero.mpr (by linarith)))] linarith [hxA.1] have hconst : IntegrableOn (fun _ : Ω => -q) A mu := integrableOn_const hfin.ne have hupperSlice : (∫ x in A, f x ∂mu) ≤ -q * (mu A).toReal := by calc (∫ x in A, f x ∂mu) ≤ ∫ _ in A, -q ∂mu := integral_mono_ae hfA hconst (ae_restrict_iff' hA |>.2 <| by filter_upwards with x hx exact hx.2.le) _ = -q * (mu A).toReal := by rw [setIntegral_const] simp [Measure.real] ring have hlowerInt : -(mu A).toReal ≤ ∫ x in A, f x ∂mu := by have := hdom A hA linarith [neg_abs_le (∫ x in A, f x ∂mu)] have hzeroReal : (mu A).toReal = 0 := by have hnonneg : 0 ≤ (mu A).toReal := ENNReal.toReal_nonneg nlinarith have hzero : mu A = 0 := by rw [ENNReal.toReal_eq_zero_iff] at hzeroReal exact hzeroReal.resolve_right hfin.ne rw [ae_iff] simpa [A] using hzero rw [← ae_all_iff] at hslice filter_upwards [hslice] with x hx by_contra hqx have hfxq : f x < -q := lt_of_not_ge hqx obtain ⟨m, hm⟩ := exists_nat_ge (-f x) exact hx m ⟨by linarith, hfxq⟩ have hupperOne : ∀ᵐ x ∂mu, f x ≤ 1 := by have hq := fun j : ℕ => hupper (1 + 1 / ((j + 1 : ℕ) : ℝ)) (by have : 0 < 1 / ((j + 1 : ℕ) : ℝ) := by positivity linarith) rw [← ae_all_iff] at hq filter_upwards [hq] with x hx by_contra hx1 have hpos : 0 < f x - 1 := sub_pos.mpr (lt_of_not_ge hx1) obtain ⟨j, hj⟩ := exists_nat_one_div_lt hpos have hxj := hx j norm_num [Nat.cast_add, cast_one] at hxj have hj' : ((j : ℝ) + 1)⁻¹ < f x - 1 := by simpa [one_div] using hj linarith have hlowerOne : ∀ᵐ x ∂mu, -1 ≤ f x := by have hq := fun j : ℕ => hlower (1 + 1 / ((j + 1 : ℕ) : ℝ)) (by have : 0 < 1 / ((j + 1 : ℕ) : ℝ) := by positivity linarith) rw [← ae_all_iff] at hq filter_upwards [hq] with x hx by_contra hx1 have hlt : f x < -1 := lt_of_not_ge hx1 have hpos : 0 < -f x - 1 := by linarith obtain ⟨j, hj⟩ := exists_nat_one_div_lt hpos have hxj := hx j norm_num [Nat.cast_add, cast_one] at hxj have hj' : ((j : ℝ) + 1)⁻¹ < -f x - 1 := by simpa [one_div] using hj linarith filter_upwards [hupperOne, hlowerOne] with x hxU hxL exact abs_le.mpr ⟨by linarith, hxU⟩

theorem sSup_image_eq_of_dense_tendsto {ι : Type*} (F : ι → ℝ) (S D : Set ι) (hDS : D ⊆ S) (hbdd : BddAbove (F '' S)) (hdense : ∀ x ∈ S, ∃ seq : ℕ → ι, (∀ j, seq j ∈ D) ∧ Tendsto (fun j => F (seq j)) atTop (nhds (F x))) : sSup (F '' S) = sSup (F '' D) := by classical by_cases hS : S = ∅ · have hD : D = ∅ := Set.eq_empty_of_subset_empty (by simpa [hS] using hDS) simp [hS, hD] · obtain ⟨x0, hx0⟩ := Set.nonempty_iff_ne_empty.mpr hS obtain ⟨seq, hseqD, _⟩ := hdense x0 hx0 have hDne : D.Nonempty := ⟨seq 0, hseqD 0⟩ have himageDne : (F '' D).Nonempty := hDne.image F have hbddD : BddAbove (F '' D) := hbdd.mono (Set.image_mono hDS) apply le_antisymm · refine csSup_le (Set.image_nonempty.mpr ⟨x0, hx0⟩) ?_ rintro y ⟨x, hx, rfl⟩ obtain ⟨seq, hseqD, htendsto⟩ := hdense x hx refine le_of_tendsto htendsto (Filter.Eventually.of_forall fun j => ?_) exact le_csSup hbddD ⟨seq j, hseqD j, rfl⟩ · exact csSup_le_csSup hbdd himageDne (Set.image_mono hDS)

theorem measurable_sSup_image_of_countable_dense {Ω ι : Type*} [MeasurableSpace Ω] (S D : Set ι) (F : Ω → ι → ℝ) (hD : D.Countable) (hF : ∀ π ∈ D, Measurable (fun ω => F ω π)) (heq : ∀ ω, sSup ((fun π => F ω π) '' S) = sSup ((fun π => F ω π) '' D)) : Measurable (fun ω => sSup ((fun π => F ω π) '' S)) := by classical let _ : Countable D := hD.to_subtype have hsup : Measurable (fun ω : Ω => ⨆ π : D, F ω π.1) := Measurable.iSup (fun π => hF π.1 π.2) convert hsup using 1 ext ω rw [heq ω] have himage : ((fun π : ι => F ω π) '' D) = ((fun π : D => F ω π.1) '' univ) := by ext y constructor · rintro ⟨π, hπ, rfl⟩ exact ⟨⟨π, hπ⟩, Set.mem_univ _, rfl⟩ · rintro ⟨π, _hπ, rfl⟩ exact ⟨π.1, π.2, rfl⟩ rw [himage] have huniv : ((fun π : D => F ω π.1) '' univ) = range (fun π : D => F ω π.1) := by ext y constructor · rintro ⟨π, _hπ, rfl⟩ exact ⟨π, rfl⟩ · rintro ⟨π, rfl⟩ exact ⟨π, Set.mem_univ _, rfl⟩ rw [huniv, sSup_range]

theorem bddAbove_image_of_bound {Ω ι : Type*} (S : Set ι) (F : Ω → ι → ℝ) (C : ℝ) (hbound : ∀ ω, ∀ π ∈ S, F ω π ≤ C) (ω : Ω) : BddAbove ((fun π => F ω π) '' S) := by exact bddAbove_def.mpr ⟨C, by rintro _ ⟨π, hπ, rfl⟩ exact hbound ω π hπ⟩