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

PL1/NoiseGenerator.lean

All source files · Download exact source

SHA-256: 678335be02293235f30badc465bc2f78f19ba2a6ed2388d52a1d4c7508a88275

1import PL1.ResolventAlmostInvariant2import PL1.ResolventGeneratorGraph3import Mathlib.Analysis.Calculus.Deriv.Slope4import Mathlib.Analysis.SpecialFunctions.ExpDeriv56/-! # The genuine infinitesimal generator of the product-noise semigroup78The generator is defined by the right norm derivative of the actual Haar L19semigroup. Uniform bounds on resolvent difference quotients and the dense10Walsh family identify its domain with the concrete resolvent graph.11-/1213noncomputable section14open Filter MeasureTheory15open scoped Topology ENNReal NNReal16namespace PL1.Noise17open Walsh1819variable (K : Type*) [RCLike K] (rates : ℕ → ℝ≥0)2021/-- The actual right difference quotient of the noise semigroup. -/22def generatorQuotient (u : ℝ≥0) : Lp K 1 haar →L[K] Lp K 1 haar :=23  (u : ℝ)⁻¹ • (noiseL1 K rates u - ContinuousLinearMap.id K (Lp K 1 haar))2425@[simp] theorem generatorQuotient_apply (u : ℝ≥0) (f : Lp K 1 haar) :26    generatorQuotient K rates u f = (u : ℝ)⁻¹ • (noiseL1 K rates u f - f) := rfl2728/-- `g` is the positive generator applied to `f`, so the semigroup derivative equals `-g`. -/29def IsGeneratorPair (f g : Lp K 1 haar) : Prop :=30  Tendsto (fun u : ℝ≥0 => generatorQuotient K rates u f) (𝓝[>] 0) (𝓝 (-g))3132/-- Resolvent-regularized difference quotients, with the unit resolvent used in the graph. -/33def regularizedQuotient (u : ℝ≥0) : Lp K 1 haar →L[K] Lp K 1 haar :=34  (u : ℝ)⁻¹ • ((noiseL1 K rates u).comp (resolventL1 K rates (dyadicTime 0)) -35    resolventL1 K rates (dyadicTime 0))3637theorem regularizedQuotient_apply (u : ℝ≥0) (f : Lp K 1 haar) :38    regularizedQuotient K rates u f =39      generatorQuotient K rates u (resolventL1 K rates (dyadicTime 0) f) := rfl4041/-- The operator family is uniformly bounded even at the zero endpoint. -/42theorem norm_regularizedQuotient_le (u : ℝ≥0) : ‖regularizedQuotient K rates u‖ ≤ 2 := by43  by_cases hu : u = 044  · simp [regularizedQuotient, hu]45  have hu0 : (0 : ℝ) < u := by exact_mod_cast (pos_iff_ne_zero.mpr hu)46  rw [regularizedQuotient, norm_smul, Real.norm_of_nonneg (inv_nonneg.mpr u.coe_nonneg)]47  apply (mul_le_mul_of_nonneg_left (norm_noise_comp_resolvent_sub_le_time K rates (dyadicTime 0) u)48    (inv_nonneg.mpr u.coe_nonneg)).trans_eq49  simp only [dyadicTime, pow_zero, Subtype.coe_mk, div_one]50  field_simp5152private theorem tendsto_exp_quotient (lam : ℝ) :53    Tendsto (fun u : ℝ≥0 => (u : ℝ)⁻¹ * (Real.exp (-(u : ℝ) * lam) - 1))54      (𝓝[>] 0) (𝓝 (-lam)) := by55  have hd : HasDerivAt (fun u : ℝ => Real.exp (-u * lam)) (-lam) 0 := by56    convert (((hasDerivAt_id (0 : ℝ)).neg.mul_const lam).exp) using 1 <;> simp57  have ht := hd.tendsto_slope_zero_right58  have hcoe : Tendsto (fun u : ℝ≥0 => (u : ℝ)) (𝓝[>] (0 : ℝ≥0)) (𝓝[>] (0 : ℝ)) := by59    exact (NNReal.map_coe_nhdsGT 0).le60  simpa only [Function.comp_def, zero_add, neg_zero, zero_mul, Real.exp_zero,61    smul_eq_mul] using ht.comp hcoe6263/-- The right norm derivative of the unit-resolvent orbit on the dense Walsh family. -/64theorem tendsto_regularizedQuotient_character (F : Finset ℕ) :65    Tendsto (fun u : ℝ≥0 => regularizedQuotient K rates u (scalarCharacterLp K 1 F))66      (𝓝[>] 0) (𝓝 ((resolventL1 K rates (dyadicTime 0) - ContinuousLinearMap.id K (Lp K 1 haar))67        (scalarCharacterLp K 1 F))) := by68  let lam := rateSum rates F69  have hden : 1 + lam ≠ 0 := ne_of_gt (by dsimp [lam]; linarith [rateSum_nonneg rates F])70  have ht := (tendsto_exp_quotient lam).mul_const ((1 + lam)⁻¹)71  have hscalar : -lam * (1 + lam)⁻¹ = (1 + lam)⁻¹ - 1 := by field_simp; ring72  rw [hscalar] at ht73  have hc := ((RCLike.continuous_ofReal : Continuous (fun x : ℝ => (x : K))).tendsto _).comp ht74  have hv := hc.smul_const (scalarCharacterLp K 1 F)75  convert hv using 176  · funext u77    simp only [Function.comp_def, regularizedQuotient, smul_apply, sub_apply, ContinuousLinearMap.comp_apply,78      resolventL1_scalarCharacter, map_smul, noiseL1_character, dyadicTime, pow_zero,79      one_mul, RCLike.real_smul_eq_coe_smul (K := K), smul_smul,80      ← sub_smul, RCLike.ofReal_mul, RCLike.ofReal_sub, RCLike.ofReal_one]81    congr 182    dsimp [lam]83    ring84  · simp only [sub_apply, ContinuousLinearMap.id_apply, resolventL1_scalarCharacter,85      dyadicTime, pow_zero, one_mul, RCLike.ofReal_sub, RCLike.ofReal_one,86      sub_smul, one_smul, lam]8788/-- Every resolvent image has the actual right norm derivative given by its resolvent equation. -/89theorem tendsto_generatorQuotient_resolvent (f : Lp K 1 haar) :90    Tendsto (fun u : ℝ≥0 => generatorQuotient K rates u (resolventL1 K rates (dyadicTime 0) f))91      (𝓝[>] 0) (𝓝 (resolventL1 K rates (dyadicTime 0) f - f)) := by92  exact tendsto_apply_of_dense_span (scalarCharacterLp K 1)93    (dense_span_scalarCharacterLp K 1 (by norm_num)) (regularizedQuotient K rates)94    (resolventL1 K rates (dyadicTime 0) - ContinuousLinearMap.id K (Lp K 1 haar)) (𝓝[>] 0)95    2 (norm_regularizedQuotient_le K rates) (tendsto_regularizedQuotient_character K rates) f9697#print axioms tendsto_generatorQuotient_resolvent98end PL1.Noise99100namespace PL1.Noise101open Walsh102variable (K : Type*) [RCLike K] (rates : ℕ → ℝ≥0)103104/-- Resolvents commute with the genuine difference quotients, including the zero endpoint. -/105theorem resolvent_generatorQuotient (t : PositiveTime) (u : ℝ≥0) (f : Lp K 1 haar) :106    resolventL1 K rates t (generatorQuotient K rates u f) =107      generatorQuotient K rates u (resolventL1 K rates t f) := by108  simp only [generatorQuotient_apply, RCLike.real_smul_eq_coe_smul (K := K), map_smul, map_sub]109  congr 2110  exact (DFunLike.congr_fun (noiseL1_resolvent_commute K rates u t) f).symm111112/-- The right norm derivative and the concrete resolvent graph give exactly the same pairs. -/113theorem isGeneratorPair_iff_resolvent (f g : Lp K 1 haar) :114    IsGeneratorPair K rates f g ↔ resolventL1 K rates (dyadicTime 0) (f + g) = f := by115  constructor116  · intro hg117    have ht := ((resolventL1 K rates (dyadicTime 0)).continuous.tendsto (-g)).comp hg118    have ht' : Tendsto (fun u : ℝ≥0 => generatorQuotient K rates u119        (resolventL1 K rates (dyadicTime 0) f)) (𝓝[>] 0)120        (𝓝 (-resolventL1 K rates (dyadicTime 0) g)) := by121      simpa only [Function.comp_def, resolvent_generatorQuotient, map_neg] using ht122    have he := tendsto_nhds_unique (tendsto_generatorQuotient_resolvent K rates f) ht'123    rw [map_add]124    apply sub_eq_zero.mp125    calc126      _ = (resolventL1 K rates (dyadicTime 0) f - f) +127          resolventL1 K rates (dyadicTime 0) g := by abel128      _ = 0 := by rw [he, neg_add_cancel]129  · intro he130    have ht := tendsto_generatorQuotient_resolvent K rates (f + g)131    simpa only [IsGeneratorPair, he, sub_add_eq_sub_sub, sub_self, zero_sub] using ht132133#print axioms isGeneratorPair_iff_resolvent134end PL1.Noise135136namespace PL1.Noise137open Walsh138variable (K : Type*) [RCLike K] (rates : ℕ → ℝ≥0)139140/-- The concrete graph is exactly the graph of the genuine positive infinitesimal generator. -/141theorem isGeneratorPair_iff_mem_graph (f g : Lp K 1 haar) :142    IsGeneratorPair K rates f g ↔ (f, g) ∈ ResolventGeneratorGraph.graph K rates :=143  isGeneratorPair_iff_resolvent K rates f g144145/-- Positive-time resolvents map every L1 function into the genuine generator domain. -/146theorem isGeneratorPair_resolvent (t : PositiveTime) (f : Lp K 1 haar) :147    IsGeneratorPair K rates (resolventL1 K rates t f)148      ((((t : ℝ)⁻¹ : ℝ) : K) • (f - resolventL1 K rates t f)) :=149  (isGeneratorPair_iff_mem_graph K rates _ _).mpr150    (ResolventGeneratorGraph.resolvent_pair_mem K rates t f)151152/-- The generator's value is unique; no choice of derivative is built into the graph. -/153theorem IsGeneratorPair.unique {f g h : Lp K 1 haar}154    (hg : IsGeneratorPair K rates f g) (hh : IsGeneratorPair K rates f h) : g = h :=155  ResolventGeneratorGraph.snd_unique K rates156    ((isGeneratorPair_iff_mem_graph K rates f g).mp hg)157    ((isGeneratorPair_iff_mem_graph K rates f h).mp hh)158159/-- The generator domain is precisely the range of the actual unit resolvent. -/160theorem exists_generatorPair_iff_range (f : Lp K 1 haar) :161    (∃ g, IsGeneratorPair K rates f g) ↔ f ∈ (resolventL1 K rates (dyadicTime 0)).range := by162  constructor163  · rintro ⟨g, hg⟩164    exact ⟨f + g, (isGeneratorPair_iff_resolvent K rates f g).mp hg⟩165  · rintro ⟨x, hx⟩166    refine ⟨x - f, (isGeneratorPair_iff_resolvent K rates f (x - f)).mpr ?_⟩167    rw [add_sub_cancel]168    exact hx169170#print axioms isGeneratorPair_iff_mem_graph171#print axioms isGeneratorPair_resolvent172end PL1.Noise173174namespace PL1.Noise175open Walsh176variable (K : Type*) [RCLike K] (rates : ℕ → ℝ≥0)177178/-- The genuine generator has dense domain in the original Haar L1 space. -/179theorem dense_generator_domain :180    Dense {f : Lp K 1 haar | ∃ g, IsGeneratorPair K rates f g} := by181  intro f182  apply isClosed_closure.mem_of_tendsto (dyadic_resolvent_strong K rates f)183  exact Eventually.of_forall (fun n => subset_closure184    ⟨_, isGeneratorPair_resolvent K rates (dyadicTime n) f⟩)185186/-- The graph of the genuine generator is closed in the original product norm. -/187theorem isClosed_generator_graph :188    IsClosed {z : Lp K 1 haar × Lp K 1 haar | IsGeneratorPair K rates z.1 z.2} := by189  simp only [isGeneratorPair_iff_resolvent]190  exact isClosed_eq ((resolventL1 K rates (dyadicTime 0)).continuous.comp191    (continuous_fst.add continuous_snd)) continuous_fst192193/-- The generator is the positive diagonal Walsh multiplier asserted in the manuscript. -/194theorem isGeneratorPair_character (F : Finset ℕ) :195    IsGeneratorPair K rates (scalarCharacterLp K 1 F)196      ((rateSum rates F : K) • scalarCharacterLp K 1 F) := by197  apply (isGeneratorPair_iff_resolvent K rates _ _).mpr198  have he : scalarCharacterLp K 1 F + (rateSum rates F : K) • scalarCharacterLp K 1 F =199      ((1 + rateSum rates F : ℝ) : K) • scalarCharacterLp K 1 F := by200    simp only [RCLike.ofReal_add, RCLike.ofReal_one, add_smul, one_smul]201  rw [he, map_smul, resolventL1_scalarCharacter, smul_smul]202  have hn : 1 + rateSum rates F ≠ 0 := ne_of_gt (by linarith [rateSum_nonneg rates F])203  simp only [dyadicTime, pow_zero, one_mul, ← RCLike.ofReal_mul, mul_inv_cancel₀ hn,204    RCLike.ofReal_one, one_smul]205206#print axioms dense_generator_domain207#print axioms isClosed_generator_graph208#print axioms isGeneratorPair_character209end PL1.Noise210