PositiveSynthesis.lean

1import BFPP.StepFunctions2import BFPP.StepAlgebra3import BFPP.ContinuousBall4import Mathlib.Analysis.Normed.Operator.Extend56/-! # Extension of positive synthesis from finite step functions78The estimates first expose density as a hypothesis. The existence theorem at9the end discharges it using `stepCombination_denseRange`.10-/1112namespace BFPP1314set_option autoImplicit false1516open Set Order17open scoped ZeroAtInfty1819universe u v20variable {ι : Type u} [LinearOrder ι] [OrderBot ι] [SuccOrder ι] [NoMaxOrder ι]21  [TopologicalSpace ι] [OrderTopology ι] [CompactIccSpace ι]22variable {K : Type v} [TopologicalSpace K] [CompactSpace K]2324noncomputable def weightedCombination (w : ι → C(K, ℝ)) : (ι →₀ ℝ) →ₗ[ℝ] C(K, ℝ) :=25  Finsupp.linearCombination ℝ w2627theorem weightedCombination_apply (w : ι → C(K, ℝ)) (c : ι →₀ ℝ) (t : K) :28    weightedCombination w c t = ∑ i ∈ c.support, c i * w i t := by29  simp [weightedCombination, Finsupp.linearCombination_apply, Finsupp.sum]3031theorem weightedCombination_norm_le (w : ι → C(K, ℝ))32    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1)33    (c : ι →₀ ℝ) : ‖weightedCombination w c‖ ≤ ‖stepCombination c‖ := by34  apply (ContinuousMap.norm_le _ (norm_nonneg _)).mpr35  intro t36  rw [Real.norm_eq_abs, weightedCombination_apply]37  apply finite_synthesis_abs_bound_finset c.support c (fun i => w i t)38    ‖stepCombination c‖ (norm_nonneg _) (hw t) (fun i _hi => hb i t)39  intro i40  rw [← stepCombination_apply]41  exact c0_abs_apply_le_norm _ i4243noncomputable def synthesisOperator (w : ι → C(K, ℝ)) : C₀(ι, ℝ) →L[ℝ] C(K, ℝ) :=44  (weightedCombination w).extendOfNorm stepCombination4546theorem synthesisOperator_stepCombination (w : ι → C(K, ℝ))47    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1)48    (hdense : DenseRange (stepCombination : (ι →₀ ℝ) → C₀(ι, ℝ))) (c : ι →₀ ℝ) :49    synthesisOperator w (stepCombination c) = weightedCombination w c := by50  apply LinearMap.extendOfNorm_eq hdense51  exact ⟨1, fun c => by simpa only [one_mul] using weightedCombination_norm_le w hw hb c⟩5253theorem synthesisOperator_initialStep (w : ι → C(K, ℝ))54    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1)55    (hdense : DenseRange (stepCombination : (ι →₀ ℝ) → C₀(ι, ℝ))) (i : ι) :56    synthesisOperator w (initialStep i) = w i := by57  rw [← stepCombination_single i, synthesisOperator_stepCombination w hw hb hdense]58  simp [weightedCombination, Finsupp.linearCombination_single]5960theorem synthesisOperator_norm_le (w : ι → C(K, ℝ))61    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1)62    (hdense : DenseRange (stepCombination : (ι →₀ ℝ) → C₀(ι, ℝ))) :63    ‖synthesisOperator w‖ ≤ 1 := by64  apply LinearMap.opNorm_extendOfNorm_le hdense (by norm_num)65  intro c66  simpa only [one_mul] using weightedCombination_norm_le w hw hb c6768theorem synthesisOperator_nonexpansive (w : ι → C(K, ℝ))69    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1)70    (hdense : DenseRange (stepCombination : (ι →₀ ℝ) → C₀(ι, ℝ))) :71    LipschitzWith 1 (synthesisOperator w) := by72  apply LipschitzWith.of_dist_le_mul73  intro f g74  simp only [NNReal.coe_one, one_mul, dist_eq_norm, ← map_sub]75  calc76    ‖synthesisOperator w (f - g)‖ ≤ ‖synthesisOperator w‖ * ‖f - g‖ :=77      (synthesisOperator w).le_opNorm _78    _ ≤ 1 * ‖f - g‖ := mul_le_mul_of_nonneg_right79      (synthesisOperator_norm_le w hw hb hdense) (norm_nonneg _)80    _ = ‖f - g‖ := one_mul _8182theorem weightedCombination_bounds (w : ι → C(K, ℝ))83    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1)84    (c : ι →₀ ℝ) (m M : ℝ) (hm : m ≤ 0) (hM : 0 ≤ M)85    (hf : ∀ i, m ≤ stepCombination c i ∧ stepCombination c i ≤ M) (t : K) :86    m ≤ weightedCombination w c t ∧ weightedCombination w c t ≤ M := by87  rw [weightedCombination_apply]88  apply finite_synthesis_bounds_finset c.support c (fun i => w i t) m M hm hM89    (hw t) (fun i _hi => hb i t)90  intro i91  simpa only [stepCombination_apply] using hf i9293/-- Uniform approximation extends the finite order estimates, including positivity. -/94theorem synthesisOperator_preserves_bounds (w : ι → C(K, ℝ))95    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1)96    (hdense : DenseRange (stepCombination : (ι →₀ ℝ) → C₀(ι, ℝ)))97    (f : C₀(ι, ℝ)) (m M : ℝ) (hm : m ≤ 0) (hM : 0 ≤ M)98    (hf : ∀ i, m ≤ f i ∧ f i ≤ M) (t : K) :99    m ≤ synthesisOperator w f t ∧ synthesisOperator w f t ≤ M := by100  have happrox : ∀ ε : ℝ, 0 < ε → m - ε ≤ synthesisOperator w f t ∧101      synthesisOperator w f t ≤ M + ε := by102    intro ε hε103    obtain ⟨c, hc⟩ := Metric.denseRange_iff.mp hdense f (ε / 3) (by linarith)104    have hstep : ∀ i, m - ε / 3 ≤ stepCombination c i ∧ stepCombination c i ≤ M + ε / 3 := by105      intro i106      have hi := c0_abs_sub_le_dist f (stepCombination c) i107      have hib := abs_le.mp (hi.trans hc.le)108      have hfi := hf i109      exact ⟨by linarith, by linarith⟩110    have hfinite := weightedCombination_bounds w hw hb c (m - ε / 3) (M + ε / 3)111      (by linarith) (by linarith) hstep t112    have hlip := (synthesisOperator_nonexpansive w hw hb hdense).dist_le_mul f (stepCombination c)113    simp only [NNReal.coe_one, one_mul] at hlip114    have hp := continuousMap_abs_sub_le_dist (synthesisOperator w f)115      (synthesisOperator w (stepCombination c)) t116    have hdiff := abs_le.mp (hp.trans (hlip.trans hc.le))117    rw [synthesisOperator_stepCombination w hw hb hdense] at hdiff118    exact ⟨by linarith, by linarith⟩119  constructor120  · apply le_of_forall_pos_le_add121    intro ε hε122    have h := (happrox ε hε).1123    linarith124  · apply le_of_forall_pos_le_add125    intro ε hε126    exact (happrox ε hε).2127128theorem synthesisOperator_positive (w : ι → C(K, ℝ))129    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1)130    (hdense : DenseRange (stepCombination : (ι →₀ ℝ) → C₀(ι, ℝ)))131    (f : C₀(ι, ℝ)) (hf : ∀ i, 0 ≤ f i) (t : K) : 0 ≤ synthesisOperator w f t := by132  have hbounds : ∀ i, 0 ≤ f i ∧ f i ≤ ‖f‖ := fun i =>133    ⟨hf i, (le_abs_self _).trans (c0_abs_apply_le_norm f i)⟩134  exact (synthesisOperator_preserves_bounds w hw hb hdense f 0 ‖f‖ le_rfl135    (norm_nonneg _) hbounds t).1136137theorem synthesisOperator_zero_at (w : ι → C(K, ℝ))138    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1)139    (hdense : DenseRange (stepCombination : (ι →₀ ℝ) → C₀(ι, ℝ)))140    (t : K) (ht : ∀ i, w i t = 0) (f : C₀(ι, ℝ)) : synthesisOperator w f t = 0 := by141  refine hdense.induction_on f ?_ ?_142  · exact isClosed_eq ((ContinuousMap.evalCLM ℝ t).continuous.comp (synthesisOperator w).continuous)143      continuous_const144  · intro c145    rw [synthesisOperator_stepCombination w hw hb hdense, weightedCombination_apply]146    simp [ht]147148theorem synthesisOperator_lower_on_initialSegment (w : ι → C(K, ℝ))149    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1)150    (f : C₀(ι, ℝ)) (hf : ∀ i, 0 ≤ f i) (a : ι) (t : K) (hwt : w a t = 1)151    (L : ℝ) (hL : ∀ i, i ≤ a → L ≤ f i) : L ≤ synthesisOperator w f t := by152  have hp : ∀ i, 0 ≤ (f - L • initialStep a) i := by153    intro i154    simp only [ZeroAtInftyContinuousMap.sub_apply, ZeroAtInftyContinuousMap.smul_apply,155      initialStep_apply, smul_eq_mul]156    by_cases hi : i ≤ a157    · simp only [if_pos hi, mul_one]158      exact sub_nonneg.mpr (hL i hi)159    · simpa only [if_neg hi, mul_zero, sub_zero] using hf i160  have h := synthesisOperator_positive w hw hb stepCombination_denseRange161    (f - L • initialStep a) hp t162  rw [map_sub, map_smul, synthesisOperator_initialStep w hw hb stepCombination_denseRange] at h163  simp only [ContinuousMap.sub_apply, ContinuousMap.smul_apply, smul_eq_mul, hwt, mul_one] at h164  linarith165166theorem positiveSynthesis_exists (w : ι → C(K, ℝ))167    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1) :168    ∃ S : C₀(ι, ℝ) →L[ℝ] C(K, ℝ), ‖S‖ ≤ 1 ∧169      (∀ f, (∀ i, 0 ≤ f i) → ∀ t, 0 ≤ S f t) ∧ (∀ i, S (initialStep i) = w i) :=170  ⟨synthesisOperator w,171    synthesisOperator_norm_le w hw hb stepCombination_denseRange,172    synthesisOperator_positive w hw hb stepCombination_denseRange,173    synthesisOperator_initialStep w hw hb stepCombination_denseRange⟩174175theorem positiveSynthesis_unique (S T : C₀(ι, ℝ) →L[ℝ] C(K, ℝ))176    (h : ∀ i, S (initialStep i) = T (initialStep i)) : S = T := by177  apply ContinuousLinearMap.ext178  intro f179  refine stepCombination_denseRange.induction_on f ?_ ?_180  · exact isClosed_eq S.continuous T.continuous181  · intro c182    rw [stepCombination_eq_sum, map_sum, map_sum]183    apply Finset.sum_congr rfl184    intro i _hi185    rw [map_smul, map_smul, h i]186187end BFPP

SHA-256