OAI/Probability/GammaPassage/ResamplingEnergyIdentity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.EnergyIdentity.exponential_square_difference line 9
2. lemma OAI.GammaFPP.EnergyIdentity.exponential_square_difference_split line 22
3. theorem OAI.GammaFPP.EnergyIdentity.exponential_resampling_energy_split line 39

   Source documentation

   Exchanging a coordinate identifies the backward exponential energy with the forward one. The weighting belongs to the old environment in each term.

   theorem exponential_resampling_energy_split {ι : Type*} [Fintype ι] [DecidableEq ι]
       (μ : Measure ℝ) [IsProbabilityMeasure μ] (f : (ι → ℝ) → ℝ) (hf : Measurable f)
       (i : ι) (a : ℝ) :
       (∫⁻ z : (ι → ℝ) × (ι → ℝ), ENNReal.ofReal
         ((exp (a*f (Function.update z.1 i (z.2 i))/2)-exp (a*f z.1/2))^2)
         ∂(Measure.pi (fun _ : ι => μ)).prod (Measure.pi (fun _ : ι => μ))) =
       2 * (∫⁻ z : (ι → ℝ) × (ι → ℝ), ENNReal.ofReal
         (exp (a*f z.1)*(exp (a*max (f (Function.update z.1 i (z.2 i))-f z.1) 0/2)-1)^2)
         ∂(Measure.pi (fun _ : ι => μ)).prod (Measure.pi (fun _ : ι => μ))) := by
   …