On complemented subspaces of L1[0,1]L_1[0,1]

PL1/IntrinsicExposedPoint.lean

All source files · Download exact source

SHA-256: a78e0fb712ef15e897d8ff8889c1cb78a54c27401e15ba212c655869264d2fe8

1import PL1.IntrinsicTailNorm23/-!4# The constant one is exposed in the actual intrinsic unit ball56The exposing functional is the Haar integral of the zeroth coordinate.7Positive rates force every resolvent-fixed L1 function to be constant; this8is proved by strong convergence of resolvent iterates on the dense Walsh span.9-/1011noncomputable section12open MeasureTheory Filter13open scoped ENNReal NNReal Topology BigOperators1415namespace PL1.IntrinsicExposedPoint16open Walsh WalshExpectations Noise IntrinsicGraph IntrinsicTailNorm1718variable (K : Type*) [RCLike K]1920def meanL1 : Lp K 1 haar →L[K] K := L1.integralCLM' K2122theorem meanL1_apply (f : Lp K 1 haar) : meanL1 K f = ∫ x, f x ∂haar := by23  rw [meanL1, ← L1.integral_eq']24  exact L1.integral_eq_integral f2526theorem norm_meanL1_apply_le (f : Lp K 1 haar) : ‖meanL1 K f‖ ≤ ‖f‖ := by27  rw [meanL1, ← L1.integral_eq']28  exact L1.norm_integral_le f2930theorem meanL1_character (F : Finset ℕ) :31    meanL1 K (scalarCharacterLp K 1 F) = if F = ∅ then 1 else 0 := by32  rw [meanL1_apply, integral_congr_ae (coeFn_scalarCharacterLp K 1 F)]33  simp only [scalarCharacter, integral_ofReal, Walsh.integral_character]34  split_ifs <;> simp3536theorem expectation_zero_eq_mean :37    expectationL1 K 0 = (meanL1 K).smulRight (scalarCharacterLp K 1 ∅) := by38  apply continuousLinearMap_ext_on_scalarCharacterL139  intro F40  simp only [expectationL1_character, Finset.range_zero, Finset.subset_empty,41    ContinuousLinearMap.smulRight_apply, meanL1_character]42  split_ifs with h43  · subst F; simp44  · simp4546def resolventIterate (rates : ℕ → ℝ≥0) (t : PositiveTime) :47    ℕ → Lp K 1 haar →L[K] Lp K 1 haar48  | 0 => ContinuousLinearMap.id K _49  | n + 1 => (resolventL1 K rates t).comp (resolventIterate rates t n)5051theorem norm_resolventIterate_le (rates : ℕ → ℝ≥0) (t : PositiveTime) (n : ℕ) :52    ‖resolventIterate K rates t n‖ ≤ 1 := by53  induction n with54  | zero => exact ContinuousLinearMap.norm_id_le55  | succ n ih =>56    exact (ContinuousLinearMap.opNorm_comp_le _ _).trans57      ((mul_le_mul_of_nonneg_right (norm_resolventL1_le_one K rates t)58        (norm_nonneg _)).trans (by simpa only [one_mul] using ih))5960theorem resolventIterate_character (rates : ℕ → ℝ≥0) (t : PositiveTime)61    (n : ℕ) (F : Finset ℕ) :62    resolventIterate K rates t n (scalarCharacterLp K 1 F) =63      ((((1 + (t : ℝ) * rateSum rates F)⁻¹) ^ n : ℝ) : K) • scalarCharacterLp K 1 F := by64  induction n with65  | zero => simp only [resolventIterate, ContinuousLinearMap.id_apply, pow_zero,66      RCLike.ofReal_one, one_smul]67  | succ n ih =>68    rw [resolventIterate, ContinuousLinearMap.comp_apply, ih, map_smul,69      resolventL1_scalarCharacter, smul_smul, ← RCLike.ofReal_mul, pow_succ]7071theorem rateSum_pos {rates : ℕ → ℝ≥0} (hrates : ∀ j, 0 < rates j)72    {F : Finset ℕ} (hF : F.Nonempty) : 0 < rateSum rates F := by73  unfold rateSum74  exact Finset.sum_pos (fun j _ => hrates j) hF7576theorem tendsto_resolventIterate (rates : ℕ → ℝ≥0) (hrates : ∀ j, 0 < rates j)77    (t : PositiveTime) (f : Lp K 1 haar) :78    Tendsto (fun n => resolventIterate K rates t n f) atTop (𝓝 (expectationL1 K 0 f)) := by79  apply tendsto_apply_of_dense_span (scalarCharacterLp K 1)80    (dense_span_scalarCharacterLp K 1 (by norm_num)) (resolventIterate K rates t)81    (expectationL1 K 0) atTop 1 (norm_resolventIterate_le K rates t)82  intro F83  by_cases hF : F = ∅84  · subst F85    simpa only [resolventIterate_character, rateSum, Finset.sum_empty, mul_zero,86      add_zero, inv_one, one_pow, RCLike.ofReal_one, one_smul,87      expectationL1_character, Finset.empty_subset, ite_true] using88      (tendsto_const_nhds : Tendsto (fun _ : ℕ => scalarCharacterLp K 1 ∅)89        atTop (𝓝 (scalarCharacterLp K 1 ∅)))90  · have hr : 0 < rateSum rates F := rateSum_pos hrates (Finset.nonempty_iff_ne_empty.mpr hF)91    have htr : 0 < (t : ℝ) * rateSum rates F := mul_pos t.property hr92    have hp := tendsto_pow_atTop_nhds_zero_of_lt_one93      (inv_nonneg.mpr (by positivity : 0 ≤ 1 + (t : ℝ) * rateSum rates F))94      (by apply (inv_lt_one₀ (by positivity : 0 < 1 + (t : ℝ) * rateSum rates F)).mpr95          nlinarith [mul_pos t.property hr])96    have hc := ((RCLike.continuous_ofReal (K := K)).tendsto 0).comp hp97    convert hc.smul_const (scalarCharacterLp K 1 F) using 198    · funext n99      rw [resolventIterate_character]100      rfl101    · simp only [expectationL1_character, Finset.range_zero, Finset.subset_empty,102        hF, ite_false, RCLike.ofReal_zero, zero_smul]103104theorem eq_mean_smul_of_resolvent_fixed (rates : ℕ → ℝ≥0)105    (hrates : ∀ j, 0 < rates j) (t : PositiveTime) (f : Lp K 1 haar)106    (hf : resolventL1 K rates t f = f) :107    f = meanL1 K f • scalarCharacterLp K 1 ∅ := by108  have hiter (n : ℕ) : resolventIterate K rates t n f = f := by109    induction n with110    | zero => rfl111    | succ n ih => rw [resolventIterate, ContinuousLinearMap.comp_apply, ih, hf]112  have h := tendsto_resolventIterate K rates hrates t f113  simp only [hiter] at h114  have he := tendsto_nhds_unique tendsto_const_nhds h115  rwa [expectation_zero_eq_mean, ContinuousLinearMap.smulRight_apply] at he116117def integralFunctional (rates : ℕ → ℝ≥0) :118    (dyadicSystem K rates).IntrinsicSpace →L[K] K :=119  (meanL1 K).comp (evalZero (dyadicSystem K rates).analysis)120121theorem integralFunctional_apply (rates : ℕ → ℝ≥0)122    (x : (dyadicSystem K rates).IntrinsicSpace) :123    integralFunctional K rates x = ∫ s, evalZero (dyadicSystem K rates).analysis x s ∂haar :=124  meanL1_apply K _125126theorem integralFunctional_constant (rates : ℕ → ℝ≥0) :127    integralFunctional K rates (intrinsicCharacter K rates ∅) = 1 := by128  simp only [integralFunctional, ContinuousLinearMap.comp_apply,129    evalZero_intrinsicCharacter, meanL1_character, ite_true]130131theorem norm_integralFunctional_apply_le (rates : ℕ → ℝ≥0)132    (x : (dyadicSystem K rates).IntrinsicSpace) :133    ‖integralFunctional K rates x‖ ≤ ‖x‖ :=134  (norm_meanL1_apply_le K _).trans (norm_evalZero_le _ x)135136theorem norm_integralFunctional (rates : ℕ → ℝ≥0) : ‖integralFunctional K rates‖ = 1 := by137  apply le_antisymm138  · apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one139    intro x140    simpa only [one_mul] using norm_integralFunctional_apply_le K rates x141  · have h := (integralFunctional K rates).le_opNorm (intrinsicCharacter K rates ∅)142    simpa only [integralFunctional_constant, norm_one, norm_intrinsicConstant, mul_one] using h143144theorem eq_one_of_norm_le_one_re_eq_one {z : K} (hz : ‖z‖ ≤ 1) (hre : RCLike.re z = 1) :145    z = 1 := by146  have hnorm : ‖z‖ = 1 := le_antisymm hz (by simpa only [hre] using RCLike.re_le_norm z)147  have he := RCLike.norm_le_re_iff_eq_norm.mp (hz.trans_eq hre.symm)148  simpa only [hnorm, RCLike.ofReal_one] using he149150/-- Equality in the integral bound leaves no positive-index intrinsic norm151mass. One nonzero coordinate weight therefore makes the resolvent fix the152underlying L1 function. -/153theorem resolvent_fixed_of_integral_maximum (rates : ℕ → ℝ≥0)154    (x : (dyadicSystem K rates).IntrinsicSpace) (hx : ‖x‖ ≤ 1)155    (hφx : RCLike.re (integralFunctional K rates x) = 1) :156    resolventL1 K rates (dyadicTime 1) (evalZero (dyadicSystem K rates).analysis x) =157      evalZero (dyadicSystem K rates).analysis x := by158  have hbase : 1 ≤ ‖evalZero (dyadicSystem K rates).analysis x‖ := by159    have h := (RCLike.re_le_norm (integralFunctional K rates x)).trans (norm_meanL1_apply_le K _)160    rwa [hφx] at h161  have hsum := (IntrinsicSpikeEstimates.summable_norm_coord x).sum_le_tsum162    ({0, 1} : Finset ℕ) (fun _ _ => norm_nonneg _)163  rw [← norm_eq_tsum] at hsum164  simp only [Finset.sum_pair (by norm_num : (0:ℕ) ≠ 1)] at hsum165  have hz : coord (dyadicSystem K rates).analysis 1 x = 0 := by166    apply norm_eq_zero.mp167    change ‖evalZero (dyadicSystem K rates).analysis x‖ +168      ‖coord (dyadicSystem K rates).analysis 1 x‖ ≤ ‖x‖ at hsum169    linarith [norm_nonneg (coord (dyadicSystem K rates).analysis 1 x)]170  rw [coord_eq] at hz171  change (((ResolventEstimates.dyadicRatio ^ 1)⁻¹ : ℝ) : K) •172    (evalZero (dyadicSystem K rates).analysis x -173      resolventL1 K rates (dyadicTime 1) (evalZero (dyadicSystem K rates).analysis x)) = 0 at hz174  have hcoef : (((ResolventEstimates.dyadicRatio ^ 1)⁻¹ : ℝ) : K) ≠ 0 := by175    exact_mod_cast inv_ne_zero (pow_ne_zero _ ResolventEstimates.dyadicRatio_pos.ne')176  exact (sub_eq_zero.mp ((smul_eq_zero.mp hz).resolve_left hcoef)).symm177178/-- The Haar integral exposes exactly the constant one in the original179intrinsic unit ball whenever every rate is strictly positive. -/180theorem integralFunctional_exposes_constant (rates : ℕ → ℝ≥0)181    (hrates : ∀ j, 0 < rates j)182    (x : (dyadicSystem K rates).IntrinsicSpace) (hx : ‖x‖ ≤ 1)183    (hφx : RCLike.re (integralFunctional K rates x) = 1) :184    x = intrinsicCharacter K rates ∅ := by185  have hfixed := resolvent_fixed_of_integral_maximum K rates x hx hφx186  have hmean := eq_mean_smul_of_resolvent_fixed K rates hrates (dyadicTime 1) _ hfixed187  have hone := eq_one_of_norm_le_one_re_eq_one K188    ((norm_integralFunctional_apply_le K rates x).trans hx) hφx189  apply evalZero_injective (dyadicSystem K rates).analysis190  rw [evalZero_intrinsicCharacter]191  change meanL1 K (evalZero (dyadicSystem K rates).analysis x) = 1 at hone192  simpa only [hone, one_smul] using hmean193194theorem schurRates_strictlyPositive (j : ℕ) : 0 < schurRates j := by195  change (0 : ℝ) < Real.sqrt (Real.log (j + 2))196  apply Real.sqrt_pos.mpr197  apply Real.log_pos198  have hj : (0 : ℝ) ≤ j := Nat.cast_nonneg j199  linarith200201theorem integralFunctional_maximum_iff (rates : ℕ → ℝ≥0)202    (hrates : ∀ j, 0 < rates j) (x : (dyadicSystem K rates).IntrinsicSpace)203    (hx : ‖x‖ ≤ 1) :204    RCLike.re (integralFunctional K rates x) = 1 ↔ x = intrinsicCharacter K rates ∅ := by205  constructor206  · exact integralFunctional_exposes_constant K rates hrates x hx207  · intro he208    rw [he, integralFunctional_constant, RCLike.one_re]209210theorem integralFunctional_strict_maximum (rates : ℕ → ℝ≥0)211    (hrates : ∀ j, 0 < rates j) (x : (dyadicSystem K rates).IntrinsicSpace)212    (hx : ‖x‖ ≤ 1) (hxc : x ≠ intrinsicCharacter K rates ∅) :213    RCLike.re (integralFunctional K rates x) < 1 := by214  apply lt_of_le_of_ne215    ((RCLike.re_le_norm _).trans ((norm_integralFunctional_apply_le K rates x).trans hx))216  intro h217  exact hxc (integralFunctional_exposes_constant K rates hrates x hx h)218219theorem schur_integralFunctional_exposes_constant220    (x : (dyadicSystem K schurRates).IntrinsicSpace) (hx : ‖x‖ ≤ 1)221    (hφx : RCLike.re (integralFunctional K schurRates x) = 1) :222    x = intrinsicCharacter K schurRates ∅ :=223  integralFunctional_exposes_constant K schurRates schurRates_strictlyPositive x hx hφx224225theorem constant_integralFunctional_exposes_constant226    (x : (dyadicSystem K constantRates).IntrinsicSpace) (hx : ‖x‖ ≤ 1)227    (hφx : RCLike.re (integralFunctional K constantRates x) = 1) :228    x = intrinsicCharacter K constantRates ∅ :=229  integralFunctional_exposes_constant K constantRates (fun _ => zero_lt_one) x hx hφx230231end PL1.IntrinsicExposedPoint232