SynthesisIntegral.lean

1import BFPP.SynthesisMeasure23/-! # Representation on all of C₀ by continuity and step-function density -/45namespace BFPP67set_option autoImplicit false8open Set Order MeasureTheory9open scoped ZeroAtInfty CompactlySupported1011universe u v12variable {ι : Type u} [TopologicalSpace ι] [MeasurableSpace ι] [BorelSpace ι]1314noncomputable def c0IntegralLinear (μ : Measure ι) [IsFiniteMeasure μ] : C₀(ι, ℝ) →ₗ[ℝ] ℝ where15  toFun f := ∫ i, f i ∂μ16  map_add' f g := integral_add (f.toBCF.integrable μ) (g.toBCF.integrable μ)17  map_smul' c f := by simpa using integral_smul c (fun i => f i)1819noncomputable def c0Integral (μ : Measure ι) [IsFiniteMeasure μ] : C₀(ι, ℝ) →L[ℝ] ℝ :=20  (c0IntegralLinear μ).mkContinuous (μ.real univ)21    (fun f => f.toBCF.norm_integral_le_mul_norm μ)2223variable [LinearOrder ι] [OrderBot ι] [SuccOrder ι] [NoMaxOrder ι]24  [OrderTopology ι] [CompactIccSpace ι]25variable {K : Type v} [TopologicalSpace K] [CompactSpace K]2627theorem synthesisMeasure_integral (w : ι → C(K, ℝ))28    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1)29    (t : K) (f : C₀(ι, ℝ)) :30    ∫ i, f i ∂synthesisMeasure w hw hb t = synthesisOperator w f t := by31  change c0Integral (synthesisMeasure w hw hb t) f = synthesisOperator w f t32  refine stepCombination_denseRange.induction_on f ?_ ?_33  · exact isClosed_eq (c0Integral _).continuous34      ((ContinuousMap.evalCLM ℝ t).continuous.comp (synthesisOperator w).continuous)35  · intro c36    rw [stepCombination_eq_sum, map_sum, map_sum, ContinuousMap.sum_apply]37    apply Finset.sum_congr rfl38    intro i _39    rw [map_smul, map_smul, ContinuousMap.smul_apply]40    congr 141    exact synthesisMeasure_integral_compact w hw hb t (initialStepCompact i)4243/-- Full measure conclusion of the positive-synthesis lemma. -/44theorem synthesisMeasure_real_mass (w : ι → C(K, ℝ))45    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1)46    (t : K) : (synthesisMeasure w hw hb t).real univ = ⨆ i, w i t := by47  change (synthesisMeasure w hw hb t univ).toReal = _48  rw [synthesisMeasure_mass, ENNReal.toReal_iSup (fun _ => ENNReal.ofReal_ne_top)]49  apply iSup_congr50  intro i51  exact ENNReal.toReal_ofReal (hb i t).15253/-- Full measure conclusion of the positive-synthesis lemma. -/54theorem positiveSynthesis_measure_representation (w : ι → C(K, ℝ))55    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1)56    (t : K) : ∃ μ : Measure ι, μ.Regular ∧ IsFiniteMeasure μ ∧57      (∀ f : C₀(ι, ℝ), ∫ i, f i ∂μ = synthesisOperator w f t) ∧58      (∀ i, μ (Iic i) = ENNReal.ofReal (w i t)) ∧59      μ univ = ⨆ i, ENNReal.ofReal (w i t) ∧ μ univ ≤ 1 :=60  ⟨synthesisMeasure w hw hb t, inferInstance, inferInstance,61    synthesisMeasure_integral w hw hb t, synthesisMeasure_initialSegment w hw hb t,62    synthesisMeasure_mass w hw hb t, synthesisMeasure_mass_le_one w hw hb t⟩6364end BFPP

SHA-256