SynthesisMeasure.lean

1import BFPP.PositiveSynthesis2import Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real3import Mathlib.MeasureTheory.Integral.BoundedContinuousFunction45/-! # The Radon measures representing positive synthesis -/67namespace BFPP89set_option autoImplicit false10open Set Order MeasureTheory11open scoped ZeroAtInfty CompactlySupported ENNReal1213universe u v14variable {ι : Type u} [LinearOrder ι] [OrderBot ι] [SuccOrder ι] [NoMaxOrder ι]15  [TopologicalSpace ι] [OrderTopology ι] [CompactIccSpace ι]16  [MeasurableSpace ι] [BorelSpace ι]17variable {K : Type v} [TopologicalSpace K] [CompactSpace K]1819local instance synthesisIndexWeaklyLocallyCompact : WeaklyLocallyCompactSpace ι where20  exists_compact_mem_nhds i := ⟨Iic i, initialSegment_isCompact i,21    (initialSegment_isClopen i).isOpen.mem_nhds le_rfl⟩2223noncomputable def initialStepCompact (i : ι) : C_c(ι, ℝ) where24  toFun := initialStep i25  continuous_toFun := (initialStep i).continuous26  hasCompactSupport' := (initialSegment_isCompact i).of_isClosed_subset isClosed_closure27    (closure_minimal (by28      intro j hj29      by_contra h30      change ¬ j ≤ i at h31      exact hj (by simp only [initialStep_apply, if_neg h])) isClosed_Iic)3233@[simp] theorem initialStepCompact_toC0 (i : ι) :34    (initialStepCompact i : C₀(ι, ℝ)) = initialStep i := by ext; rfl3536noncomputable def synthesisFunctional (w : ι → C(K, ℝ))37    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1)38    (t : K) : C_c(ι, ℝ) →ₚ[ℝ] ℝ where39  toFun f := synthesisOperator w (f : C₀(ι, ℝ)) t40  map_add' f g := by41    change synthesisOperator w ((f : C₀(ι, ℝ)) + (g : C₀(ι, ℝ))) t = _42    simp only [map_add, ContinuousMap.add_apply]43  map_smul' c f := by44    change synthesisOperator w (c • (f : C₀(ι, ℝ))) t = _45    simp only [map_smul, ContinuousMap.smul_apply, smul_eq_mul, RingHom.id_apply]46  monotone' f g hfg := by47    have h := synthesisOperator_positive w hw hb stepCombination_denseRange48      ((g : C₀(ι, ℝ)) - (f : C₀(ι, ℝ))) (fun i => sub_nonneg.mpr (hfg i)) t49    simpa only [map_sub, ContinuousMap.sub_apply, sub_nonneg] using h5051noncomputable def synthesisMeasure (w : ι → C(K, ℝ))52    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1)53    (t : K) : Measure ι := RealRMK.rieszMeasure (synthesisFunctional w hw hb t)5455instance synthesisMeasure_regular (w : ι → C(K, ℝ))56    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1)57    (t : K) : (synthesisMeasure w hw hb t).Regular := RealRMK.regular_rieszMeasure _5859theorem synthesisFunctional_initialStep (w : ι → C(K, ℝ))60    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1)61    (t : K) (i : ι) : synthesisFunctional w hw hb t (initialStepCompact i) = w i t := by62  change synthesisOperator w (initialStepCompact i : C₀(ι, ℝ)) t = _63  rw [initialStepCompact_toC0, synthesisOperator_initialStep w hw hb stepCombination_denseRange]6465theorem synthesisMeasure_initialSegment (w : ι → C(K, ℝ))66    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1)67    (t : K) (i : ι) : synthesisMeasure w hw hb t (Iic i) = ENNReal.ofReal (w i t) := by68  rw [← synthesisFunctional_initialStep w hw hb t i]69  apply le_antisymm70  · apply RealRMK.rieszMeasure_le_of_eq_one _ (f := initialStepCompact i)71      (fun j => by change 0 ≤ initialStep i j; simp only [initialStep_apply]; split_ifs <;> norm_num)72      (initialSegment_isCompact i)73    intro j hj74    change j ≤ i at hj75    change initialStep i j = 176    simp [initialStep_apply, hj]77  · apply RealRMK.le_rieszMeasure_tsupport_subset _ (f := initialStepCompact i)78      (fun j => by79        change 0 ≤ initialStep i j ∧ initialStep i j ≤ 180        simp only [initialStep_apply]81        split_ifs <;> norm_num)82    apply closure_minimal _ isClosed_Iic83    intro j hj84    by_contra h85    change ¬ j ≤ i at h86    exact hj (by change initialStep i j = 0; simp only [initialStep_apply, if_neg h])8788/-- Inner regularity, rather than continuity of measure for an uncountable union. -/89theorem synthesisMeasure_mass (w : ι → C(K, ℝ))90    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1)91    (t : K) : synthesisMeasure w hw hb t univ = ⨆ i, ENNReal.ofReal (w i t) := by92  apply le_antisymm93  · rw [isOpen_univ.measure_eq_iSup_isCompact]94    refine iSup_le fun s => iSup_le fun _ => iSup_le fun hs => ?_95    obtain ⟨i, hi⟩ := hs.bddAbove96    exact (measure_mono hi).trans ((synthesisMeasure_initialSegment w hw hb t i).le.trans97      (le_iSup (fun j => ENNReal.ofReal (w j t)) i))98  · refine iSup_le fun i => ?_99    rw [← synthesisMeasure_initialSegment w hw hb t i]100    exact measure_mono (subset_univ _)101102theorem synthesisMeasure_mass_le_one (w : ι → C(K, ℝ))103    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1)104    (t : K) : synthesisMeasure w hw hb t univ ≤ 1 := by105  rw [synthesisMeasure_mass]106  exact iSup_le fun i => (ENNReal.ofReal_le_ofReal (hb i t).2).trans_eq ENNReal.ofReal_one107108instance synthesisMeasure_finite (w : ι → C(K, ℝ))109    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1)110    (t : K) : IsFiniteMeasure (synthesisMeasure w hw hb t) :=111  ⟨(synthesisMeasure_mass_le_one w hw hb t).trans_lt (by simp)⟩112113theorem synthesisMeasure_integral_compact (w : ι → C(K, ℝ))114    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1)115    (t : K) (f : C_c(ι, ℝ)) :116    ∫ i, f i ∂synthesisMeasure w hw hb t = synthesisOperator w (f : C₀(ι, ℝ)) t :=117  RealRMK.integral_rieszMeasure (synthesisFunctional w hw hb t) f118119end BFPP

SHA-256