Actual affine normalized Gibbs transport

Fix the true affine inverse; Transform the actual Lebesgue integrals; Cancel the Jacobian in the normalized law

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem map_affine_gibbs (F : E → ℝ) (p : E) {s : ℝ} (hs : s ≠ 0) :
    Measure.map (fun x : E => p+s • x)
      ((volume : Measure E).tilted (fun x => -F x)) =
      volume.tilted (fun x => -F (s⁻¹ • (x-p))) := by
  let T := fun x : E => p+s • x
  let H := fun x : E => s⁻¹ • (x-p)
  let J : ℝ := |(s^Module.finrank ℝ E)⁻¹|
  have hJ : J ≠ 0 := abs_ne_zero.mpr (inv_ne_zero (pow_ne_zero _ hs))
  have hm : Measurable T := by dsimp [T]; fun_prop
  have hHT (x : E) : H (T x) = x := by simp [H,T,smul_smul,hs]
  have change_variables (f : E → ℝ) : (∫ x, f (T x)) = J*(∫ x, f x) := by
    have h := Measure.integral_comp_smul (volume : Measure E) (fun x => f (p+x)) s
    simpa only [integral_add_left_eq_self,smul_eq_mul,T,J] using h
  have hZ : (∫ x, Real.exp (-F x)) = J*(∫ x, Real.exp (-F (H x))) := by
    simpa only [hHT] using change_variables (fun x => Real.exp (-F (H x)))
  ext B hB
  rw [Measure.map_apply hm hB,tilted_apply_eq_ofReal_integral' _ (hB.preimage hm),
    tilted_apply_eq_ofReal_integral' _ hB]
  congr 1
  rw [integral_div,integral_div]
  have hI : (∫ x in T ⁻¹' B, Real.exp (-F x)) =
      J*(∫ x in B, Real.exp (-F (H x))) := by
    have h := change_variables (B.indicator (fun x => Real.exp (-F (H x))))
    have he : (fun x => B.indicator (fun y => Real.exp (-F (H y))) (T x)) =
        (T ⁻¹' B).indicator (fun x => Real.exp (-F x)) := by
      funext x
      by_cases hx : T x ∈ B <;> simp [Set.indicator,hx,hHT]
    rw [he,integral_indicator (hB.preimage hm),integral_indicator hB] at h
    exact h
  rw [hI,hZ]
  exact mul_div_mul_left _ _ hJ

end
end AutoSamplingTheory.TechnicalLemmas.Measure.AffineGibbs

Exact module and namespace context