PL1/NoiseGeneratorCore.lean

All source files · Download exact source

SHA-256: 323527fcec8aee10ef1aa0f040f3b493ed038c21200e64d9a42a7b46868ca0da

1import PL1.NoiseGenerator2import PL1.WalshExpectations34/-! # Finite Walsh polynomials form a core for the actual noise generator56The conditional expectations preserve the genuine generator graph and7converge in both coordinates. Convergence is stated explicitly in the graph8sum norm `‖f‖₁ + ‖g‖₁`, with no substitution of the product maximum norm.9-/1011noncomputable section12open Filter MeasureTheory13open scoped Topology ENNReal NNReal14namespace PL1.Noise15open Walsh WalshExpectations1617variable (K : Type*) [RCLike K] (rates : ℕ → ℝ≥0)1819/-- Every finite-coordinate expectation preserves the actual infinitesimal generator graph. -/20theorem IsGeneratorPair.expectation {f g : Lp K 1 haar}21    (hfg : IsGeneratorPair K rates f g) (m : ℕ) :22    IsGeneratorPair K rates (expectationL1 K m f) (expectationL1 K m g) := by23  apply (isGeneratorPair_iff_resolvent K rates _ _).mpr24  have he := (isGeneratorPair_iff_resolvent K rates f g).mp hfg25  calc26    _ = resolventL1 K rates (dyadicTime 0) (expectationL1 K m (f + g)) := by simp only [map_add]27    _ = expectationL1 K m (resolventL1 K rates (dyadicTime 0) (f + g)) :=28      (DFunLike.congr_fun (expectationL1_resolvent_commute K m rates (dyadicTime 0)) (f + g)).symm29    _ = _ := by rw [he]3031/-- The expectation approximants converge in the exact graph sum norm. -/32theorem tendsto_expectation_graphNorm (f g : Lp K 1 haar) :33    Tendsto (fun m => ResolventGeneratorGraph.graphNorm K34      (expectationL1 K m f - f, expectationL1 K m g - g)) atTop (𝓝 0) := by35  have hf := ((tendsto_expectationL1 K f).sub_const f).norm36  have hg := ((tendsto_expectationL1 K g).sub_const g).norm37  simpa only [ResolventGeneratorGraph.graphNorm, sub_self, norm_zero, zero_add] using hf.add hg3839/-- Every actual generator pair is approximated by finite Walsh polynomial generator pairs. -/40theorem IsGeneratorPair.polynomial_core {f g : Lp K 1 haar}41    (hfg : IsGeneratorPair K rates f g) :42    (∀ m, expectationL1 K m f ∈ finiteSpan K m ∧ expectationL1 K m g ∈ finiteSpan K m ∧43      IsGeneratorPair K rates (expectationL1 K m f) (expectationL1 K m g)) ∧44    Tendsto (fun m => ‖expectationL1 K m f - f‖ + ‖expectationL1 K m g - g‖) atTop (𝓝 0) :=45  ⟨fun m => ⟨expectationL1_mem_finiteSpan K m f, expectationL1_mem_finiteSpan K m g,46      hfg.expectation K rates m⟩, tendsto_expectation_graphNorm K f g⟩4748/-- A quantitative form of graph-norm density by finite Walsh polynomials. -/49theorem IsGeneratorPair.exists_polynomial_graphNorm_lt {f g : Lp K 1 haar}50    (hfg : IsGeneratorPair K rates f g) (ε : ℝ) (hε : 0 < ε) :51    ∃ (m : ℕ) (p q : Lp K 1 haar), p ∈ finiteSpan K m ∧ q ∈ finiteSpan K m ∧52      IsGeneratorPair K rates p q ∧ ‖p - f‖ + ‖q - g‖ < ε := by53  obtain ⟨m, hm⟩ := ((tendsto_expectation_graphNorm K f g).eventually_lt_const hε).exists54  exact ⟨m, expectationL1 K m f, expectationL1 K m g,55    expectationL1_mem_finiteSpan K m f, expectationL1_mem_finiteSpan K m g,56    hfg.expectation K rates m, hm⟩5758/-- Every finite Walsh polynomial itself belongs to the actual generator domain. -/59theorem finiteSpan_subset_generator_domain (m : ℕ) {f : Lp K 1 haar}60    (hf : f ∈ finiteSpan K m) : ∃ g, IsGeneratorPair K rates f g := by61  apply (exists_generatorPair_iff_range K rates f).mpr62  have hsub : finiteSpan K m ≤ (resolventL1 K rates (dyadicTime 0)).range := by63    apply Submodule.span_le.mpr64    rintro x ⟨F, _, rfl⟩65    exact (exists_generatorPair_iff_range K rates (scalarCharacterLp K 1 F)).mp66      ⟨_, isGeneratorPair_character K rates F⟩67  exact hsub hf6869#print axioms IsGeneratorPair.polynomial_core70#print axioms IsGeneratorPair.exists_polynomial_graphNorm_lt71#print axioms finiteSpan_subset_generator_domain72end PL1.Noise73