ConvexIntegral.lean

1import BFPP.SynthesisIntegral2import BFPP.Realization34/-! # The convex-integral formula for the synthesis map56The two representing measures have combined mass at most one. Expanding the7constant part of each integral gives the displayed max/min formula in the paper.8-/910namespace BFPP1112set_option autoImplicit false13open Set Order MeasureTheory14open scoped ZeroAtInfty1516universe u v w1718/-- Reallocate the constant center among two finite measures and its remaining weight. -/19theorem convexIntegral_identity {ι : Type v} {κ : Type w}20    [MeasurableSpace ι] [MeasurableSpace κ]21    (μ : Measure ι) (ν : Measure κ) [IsFiniteMeasure μ] [IsFiniteMeasure ν]22    (c : ℝ) (f : ι → ℝ) (g : κ → ℝ) (hf : Integrable f μ) (hg : Integrable g ν) :23    c + (∫ i, f i ∂μ) - (∫ j, g j ∂ν) =24      (1 - μ.real univ - ν.real univ) * c +25        (∫ i, c + f i ∂μ) + (∫ j, c - g j ∂ν) := by26  rw [integral_add (integrable_const c) hf, integral_sub (integrable_const c) hg,27    integral_const, integral_const]28  simp only [smul_eq_mul]29  ring3031variable {K : Type u} {ι : Type v} {κ : Type w}32  [TopologicalSpace K] [CompactSpace K]33  [LinearOrder ι] [OrderBot ι] [SuccOrder ι] [NoMaxOrder ι]34  [TopologicalSpace ι] [OrderTopology ι] [CompactIccSpace ι]35  [MeasurableSpace ι] [BorelSpace ι]36  [LinearOrder κ] [OrderBot κ] [SuccOrder κ] [NoMaxOrder κ]37  [TopologicalSpace κ] [OrderTopology κ] [CompactIccSpace κ]38  [MeasurableSpace κ] [BorelSpace κ]3940namespace InseparablePair4142noncomputable abbrev positiveMeasure (F : InseparablePair K ι κ) (t : K) : Measure ι :=43  synthesisMeasure F.positive.functions F.positive.monotone F.positive.bounds t4445noncomputable abbrev negativeMeasure (F : InseparablePair K ι κ) (t : K) : Measure κ :=46  synthesisMeasure F.negative.functions F.negative.monotone F.negative.bounds t4748/-- Orthogonality forces one of the two total masses to vanish at each point. -/49theorem synthesisMass_zero_or_zero (F : InseparablePair K ι κ) (t : K) :50    (F.positiveMeasure t).real univ = 0 ∨ (F.negativeMeasure t).real univ = 0 := by51  rcases F.disjoint_channels t with hp | hn52  · left53    rw [synthesisMeasure_real_mass]54    simp [hp]55  · right56    rw [synthesisMeasure_real_mass]57    simp [hn]5859omit [SuccOrder κ] [NoMaxOrder κ] [TopologicalSpace κ] [OrderTopology κ]60  [CompactIccSpace κ] [MeasurableSpace κ] [BorelSpace κ] in61theorem positiveMass_le_one (F : InseparablePair K ι κ) (t : K) :62    (F.positiveMeasure t).real univ ≤ 1 := by63  rw [synthesisMeasure_real_mass]64  exact ciSup_le fun i => (F.positive.bounds i t).26566omit [SuccOrder ι] [NoMaxOrder ι] [TopologicalSpace ι] [OrderTopology ι]67  [CompactIccSpace ι] [MeasurableSpace ι] [BorelSpace ι] in68theorem negativeMass_le_one (F : InseparablePair K ι κ) (t : K) :69    (F.negativeMeasure t).real univ ≤ 1 := by70  rw [synthesisMeasure_real_mass]71  exact ciSup_le fun j => (F.negative.bounds j t).27273/-- The two measures and the residual atom form a probability weighting. -/74theorem synthesisMass_add_le_one (F : InseparablePair K ι κ) (t : K) :75    (F.positiveMeasure t).real univ + (F.negativeMeasure t).real univ ≤ 1 := by76  rcases F.synthesisMass_zero_or_zero t with hp | hn77  · simpa only [hp, zero_add] using F.negativeMass_le_one t78  · simpa only [hn, add_zero] using F.positiveMass_le_one t7980theorem synthesisResidualWeight_nonneg (F : InseparablePair K ι κ) (t : K) :81    0 ≤ 1 - (F.positiveMeasure t).real univ - (F.negativeMeasure t).real univ := by82  linarith [F.synthesisMass_add_le_one t]8384theorem synthesizeMap_convexIntegral (F : InseparablePair K ι κ) (z : TwoProfile ι κ)85    (t : K) :86    F.synthesizeMap z t =87      (1 - (F.positiveMeasure t).real univ - (F.negativeMeasure t).real univ) * z.center +88        (∫ i, z.center + positiveInput z i ∂F.positiveMeasure t) +89        (∫ j, z.center - negativeInput z j ∂F.negativeMeasure t) := by90  rw [synthesizeMap_apply]91  change z.center + synthesisOperator F.positive.functions (positiveInput z) t -92    synthesisOperator F.negative.functions (negativeInput z) t = _93  rw [← synthesisMeasure_integral F.positive.functions F.positive.monotone F.positive.bounds,94    ← synthesisMeasure_integral F.negative.functions F.negative.monotone F.negative.bounds]95  exact convexIntegral_identity (F.positiveMeasure t) (F.negativeMeasure t) z.center96    (positiveInput z) (negativeInput z) ((positiveInput z).toBCF.integrable _)97    ((negativeInput z).toBCF.integrable _)9899omit [MeasurableSpace ι] [BorelSpace ι] [SuccOrder κ] [NoMaxOrder κ]100  [TopologicalSpace κ] [OrderTopology κ] [CompactIccSpace κ] [MeasurableSpace κ]101  [BorelSpace κ] in102theorem center_add_positiveInput (z : TwoProfile ι κ) (i : ι) :103    z.center + positiveInput z i = max z.center (1 - z.val.1.regularizeValue i) :=104  Profile.center_add_positiveTail _ _ _ _105106omit [SuccOrder ι] [NoMaxOrder ι] [TopologicalSpace ι] [OrderTopology ι]107  [CompactIccSpace ι] [MeasurableSpace ι] [BorelSpace ι] [MeasurableSpace κ]108  [BorelSpace κ] in109theorem center_sub_negativeInput (z : TwoProfile ι κ) (j : κ) :110    z.center - negativeInput z j = min z.center (z.val.2.regularizeValue j - 1) := by111  change z.center - max (1 - z.val.2.regularizeValue j - -z.center) 0 = _112  rw [sub_neg_eq_add]113  by_cases h : 0 ≤ 1 - z.val.2.regularizeValue j + z.center114  · rw [max_eq_left h, min_eq_right (by linarith)]115    ring116  · rw [max_eq_right (le_of_not_ge h), min_eq_left (by linarith), sub_zero]117118/-- The paper's displayed convex-integral synthesis formula, with its actual measures. -/119theorem synthesizeMap_convexIntegral_max_min (F : InseparablePair K ι κ)120    (z : TwoProfile ι κ) (t : K) :121    F.synthesizeMap z t =122      (1 - (F.positiveMeasure t).real univ - (F.negativeMeasure t).real univ) * z.center +123        (∫ i, max z.center (1 - z.val.1.regularizeValue i) ∂F.positiveMeasure t) +124        (∫ j, min z.center (z.val.2.regularizeValue j - 1) ∂F.negativeMeasure t) := by125  simpa only [center_add_positiveInput, center_sub_negativeInput] using126    F.synthesizeMap_convexIntegral z t127128omit [SuccOrder κ] [NoMaxOrder κ] [TopologicalSpace κ] [OrderTopology κ]129  [CompactIccSpace κ] [MeasurableSpace κ] [BorelSpace κ] in130theorem positiveIntegrand_integrable (F : InseparablePair K ι κ)131    (z : TwoProfile ι κ) (t : K) :132    Integrable (fun i => max z.center (1 - z.val.1.regularizeValue i))133      (F.positiveMeasure t) := by134  have h : Integrable (fun i => z.center + positiveInput z i) (F.positiveMeasure t) :=135    (integrable_const z.center).add ((positiveInput z).toBCF.integrable (F.positiveMeasure t))136  simpa only [center_add_positiveInput] using h137138omit [SuccOrder ι] [NoMaxOrder ι] [TopologicalSpace ι] [OrderTopology ι]139  [CompactIccSpace ι] [MeasurableSpace ι] [BorelSpace ι] in140theorem negativeIntegrand_integrable (F : InseparablePair K ι κ)141    (z : TwoProfile ι κ) (t : K) :142    Integrable (fun j => min z.center (z.val.2.regularizeValue j - 1))143      (F.negativeMeasure t) := by144  have h : Integrable (fun j => z.center - negativeInput z j) (F.negativeMeasure t) :=145    (integrable_const z.center).sub ((negativeInput z).toBCF.integrable (F.negativeMeasure t))146  simpa only [center_sub_negativeInput] using h147148end InseparablePair149end BFPP

SHA-256