PL1/NoiseMeasures.lean
All source files · Download exact source
SHA-256: ed3e29e46e6aef0ac2463ffd38fea414e7ff3cefc1ef355e6d0214401c692e02
1import PL1.WalshModel2import Mathlib.Probability.ProductMeasure3import Mathlib.Probability.Distributions.Bernoulli4import Mathlib.MeasureTheory.Integral.Pi5import Mathlib.Analysis.SpecialFunctions.Log.Basic6import Mathlib.Tactic.Positivity7import Mathlib.Tactic.Linarith89/-!10# The actual product noise measures1112For nonnegative coordinate rates and nonnegative time, each coordinate is a13two-point probability with mean exp(-u*lambda_j). The measure on the countable14sign group is Mathlib's countable product probability, not an abstract Fourier15multiplier. Coordinates are zero based throughout.16-/1718noncomputable section19open MeasureTheory ProbabilityTheory20open scoped BigOperators ENNReal NNReal2122namespace PL1.Noise2324open Walsh2526/-- The two rate choices in the manuscript. -/27def schurRates (j : ℕ) : ℝ≥0 := ⟨Real.sqrt (Real.log (j + 2)), Real.sqrt_nonneg _⟩2829def constantRates (_ : ℕ) : ℝ≥0 := 13031/-- Coordinate expectation at time u. -/32def bias (rates : ℕ → ℝ≥0) (u : ℝ≥0) (j : ℕ) : ℝ :=33 Real.exp (-(u : ℝ) * rates j)3435theorem bias_pos (rates : ℕ → ℝ≥0) (u : ℝ≥0) (j : ℕ) : 0 < bias rates u j :=36 Real.exp_pos _3738theorem bias_le_one (rates : ℕ → ℝ≥0) (u : ℝ≥0) (j : ℕ) : bias rates u j ≤ 1 := by39 apply Real.exp_le_one_iff.mpr40 exact mul_nonpos_of_nonpos_of_nonneg (neg_nonpos.mpr u.coe_nonneg) (rates j).coe_nonneg4142def positiveProbability (rates : ℕ → ℝ≥0) (u : ℝ≥0) (j : ℕ) : unitInterval :=43 ⟨(1 + bias rates u j) / 2, by44 constructor45 · have := bias_pos rates u j46 linarith47 · have := bias_le_one rates u j48 linarith⟩4950/-- The actual biased probability on one sign coordinate. -/51def coordinateMeasure (rates : ℕ → ℝ≥0) (u : ℝ≥0) (j : ℕ) : Measure Sign :=52 bernoulliMeasure 1 (Multiplicative.ofAdd 1) (positiveProbability rates u j)5354instance (rates : ℕ → ℝ≥0) (u : ℝ≥0) (j : ℕ) :55 IsProbabilityMeasure (coordinateMeasure rates u j) := by56 unfold coordinateMeasure57 infer_instance5859/-- The countable product probability mu_u of the manuscript. -/60def measure (rates : ℕ → ℝ≥0) (u : ℝ≥0) : Measure Walsh.Group :=61 Measure.infinitePi (coordinateMeasure rates u)6263instance (rates : ℕ → ℝ≥0) (u : ℝ≥0) : IsProbabilityMeasure (measure rates u) := by64 unfold measure65 infer_instance6667theorem integral_signValue (rates : ℕ → ℝ≥0) (u : ℝ≥0) (j : ℕ) :68 ∫ a, signValue a ∂coordinateMeasure rates u j = bias rates u j := by69 rw [coordinateMeasure, integral_bernoulliMeasure]70 norm_num [signValue, positiveProbability]71 ring7273/-- The sum of rates over a finite Walsh support. -/74def rateSum (rates : ℕ → ℝ≥0) (F : Finset ℕ) : ℝ := ∑ j ∈ F, (rates j : ℝ)7576theorem rateSum_nonneg (rates : ℕ → ℝ≥0) (F : Finset ℕ) : 0 ≤ rateSum rates F :=77 Finset.sum_nonneg (fun j _ => (rates j).coe_nonneg)7879/-- Independence gives the Fourier transform of the actual product measure. -/80theorem integral_character (rates : ℕ → ℝ≥0) (u : ℝ≥0) (F : Finset ℕ) :81 ∫ x, character F x ∂measure rates u = Real.exp (-(u : ℝ) * rateSum rates F) := by82 have heq (x : Walsh.Group) : character F x = ∏ j : F, signValue (x j) := by83 exact (Finset.prod_coe_sort F (fun j => signValue (x j))).symm84 simp_rw [heq]85 change (∫ x, (fun y : F → Sign => ∏ j, signValue (y j)) (F.restrict x)86 ∂Measure.infinitePi (coordinateMeasure rates u)) = _87 rw [integral_restrict_infinitePi (coordinateMeasure rates u)88 (s := F) (f := fun y : F → Sign => ∏ j, signValue (y j))89 (continuous_of_discreteTopology.aestronglyMeasurable),90 integral_fintype_prod_eq_prod]91 simp_rw [integral_signValue]92 rw [Finset.prod_coe_sort]93 simp only [bias]94 rw [← Real.exp_sum]95 congr 196 simp [rateSum, Finset.mul_sum]9798@[simp]99theorem integral_character_constantRates (u : ℝ≥0) (F : Finset ℕ) :100 ∫ x, character F x ∂measure constantRates u = Real.exp (-(u : ℝ) * F.card) := by101 rw [integral_character]102 simp [rateSum, constantRates]103104theorem measurable_coordinateMeasure (rates : ℕ → ℝ≥0) (j : ℕ) :105 Measurable (fun u => coordinateMeasure rates u j) := by106 classical107 apply Measure.measurable_of_measurable_coe108 intro A hA109 simp only [coordinateMeasure, bernoulliMeasure_apply _ hA]110 split_ifs <;> fun_prop [positiveProbability, bias]111112/-- The product probabilities form a measurable family, so averaging them113against a time distribution is an actual measure-theoretic construction. -/114theorem measurable_measure (rates : ℕ → ℝ≥0) : Measurable (measure rates) := by115 classical116 apply Measurable.measure_of_isPiSystem_of_isProbabilityMeasure117 generateFrom_measurableCylinders.symm isPiSystem_measurableCylinders118 intro A hA119 obtain ⟨F, B, hB, rfl⟩ := (mem_measurableCylinders A).mp hA120 have hc (u : ℝ≥0) := Measure.infinitePi_cylinder121 (coordinateMeasure rates u) (s := F) (S := B) hB122 simp only [measure, hc]123 have heq (u : ℝ≥0) :124 Measure.pi (fun j : F => coordinateMeasure rates u j) B =125 ∑ x ∈ B.toFinset, ∏ j : F, coordinateMeasure rates u j {x j} := by126 simp only [← Measure.pi_singleton]127 rw [sum_measure_singleton]128 simp only [Set.coe_toFinset]129 simp only [heq]130 apply Finset.measurable_sum131 intro x hx132 apply Finset.measurable_prod133 intro j hj134 exact (Measure.measurable_coe (measurableSet_singleton _)).comp135 (measurable_coordinateMeasure rates j)136137/-- The concrete Markov kernel u ↦ mu_u. -/138def kernel (rates : ℕ → ℝ≥0) : Kernel ℝ≥0 Walsh.Group where139 toFun := measure rates140 measurable' := measurable_measure rates141142@[simp]143theorem kernel_apply (rates : ℕ → ℝ≥0) (u : ℝ≥0) : kernel rates u = measure rates u := rfl144145instance (rates : ℕ → ℝ≥0) : IsMarkovKernel (kernel rates) where146 isProbabilityMeasure u := inferInstanceAs (IsProbabilityMeasure (measure rates u))147148end PL1.Noise149