Built with Alectryon, running Lean4 v4.19.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
/- - Created in 2024 by Gaëtan Serré-//-- https://github.com/gaetanserre/SBS-Proofs-/import Mathlib.MeasureTheory.Function.Jacobian
import SBSProofs.Measure
import SBSProofs.Utils
open ENNReal
open MeasureTheory MeasureTheory.Measure
/-- Expression of the (supposed for now) density of a pushforward measure.-/noncomputabledef push_forward_density {α : Type*}
[NormedAddCommGroup α] [Module ℝ α] [MeasureSpace α]
(μ : DensityMeasure α) (μ_t : Pushforward_Measure α α)
(_ : μ_t.μ = μ.toMeasure) (T' : α → α →L[ℝ] α) :=
λ x ↦ ENNReal.ofReal |(T' x).det|* μ.d (μ_t.T_inv x)
namespace DetDerivative
variable {α β : Type*} [NormedAddCommGroup α] [NormedSpace ℝ α]
{s : Set α} (T' : α → α →L[ℝ] α)
/-- Given a map f, det (∂ₓ (f⁻¹ ∘ f) x) = 1.-/
Goals accomplished!
Goals accomplished!
Goals accomplished!🐙
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s
∀ a ∈ s, (T' a).det =1
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
(T' a).det =1
-- We prove that ∂ₓ (f⁻¹ ∘ f) = 1 using that f⁻¹ ∘ f = id, ∂ₓ id = 1 and that the derivative is unique.
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
(T' a).det =1
Goals accomplished!
Goals accomplished!🐙
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
T' a = ContinuousLinearMap.id ℝ α
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
T' a = ContinuousLinearMap.id ℝ α
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
T' a = ContinuousLinearMap.id ℝ α
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
T' a = ContinuousLinearMap.id ℝ α
Goals accomplished!
Goals accomplished!🐙
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
HasFDerivWithinAt id (ContinuousLinearMap.id ℝ α) s a
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
HasFDerivWithinAt id (ContinuousLinearMap.id ℝ α) s a
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
HasFDerivWithinAt id (ContinuousLinearMap.id ℝ α) s a
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s k2: fderivWithin ℝ id s a = ContinuousLinearMap.id ℝ α
HasFDerivWithinAt id (ContinuousLinearMap.id ℝ α) s a
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
HasFDerivWithinAt id (ContinuousLinearMap.id ℝ α) s a
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s k2: fderivWithin ℝ id s a = ContinuousLinearMap.id ℝ α
HasFDerivWithinAt id (ContinuousLinearMap.id ℝ α) s a
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s k2: fderivWithin ℝ id s a = ContinuousLinearMap.id ℝ α
HasFDerivWithinAt id (fderivWithin ℝ id s a) s a
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s k2: fderivWithin ℝ id s a = ContinuousLinearMap.id ℝ α
HasFDerivWithinAt id (fderivWithin ℝ id s a) s a
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
HasFDerivWithinAt id (ContinuousLinearMap.id ℝ α) s a
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s k2: fderivWithin ℝ id s a = ContinuousLinearMap.id ℝ α
HasFDerivWithinAt id (fderivWithin ℝ id s a) s a
Goals accomplished!
Goals accomplished!🐙
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s k2: fderivWithin ℝ id s a = ContinuousLinearMap.id ℝ α
DifferentiableWithinAt ℝ id s a
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s k2: fderivWithin ℝ id s a = ContinuousLinearMap.id ℝ α
DifferentiableWithinAt ℝ id s a
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s k2: fderivWithin ℝ id s a = ContinuousLinearMap.id ℝ α
DifferentiableWithinAt ℝ id s a
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s k2: fderivWithin ℝ id s a = ContinuousLinearMap.id ℝ α
h
HasFDerivWithinAt id (T' a) s a
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s k2: fderivWithin ℝ id s a = ContinuousLinearMap.id ℝ α
DifferentiableWithinAt ℝ id s a
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s k2: fderivWithin ℝ id s a = ContinuousLinearMap.id ℝ α
h
HasFDerivWithinAt id (T' a) s a
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s k2: fderivWithin ℝ id s a = ContinuousLinearMap.id ℝ α
h
HasFDerivWithinAt (f_inv ∘ f) (T' a) s a
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s k2: fderivWithin ℝ id s a = ContinuousLinearMap.id ℝ α
h
HasFDerivWithinAt (f_inv ∘ f) (T' a) s a
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s k2: fderivWithin ℝ id s a = ContinuousLinearMap.id ℝ α
DifferentiableWithinAt ℝ id s a
Goals accomplished!
Goals accomplished!🐙
Goals accomplished!
Goals accomplished!🐙
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
HasFDerivWithinAt id (ContinuousLinearMap.id ℝ α) s a
Goals accomplished!
Goals accomplished!🐙
Goals accomplished!
Goals accomplished!🐙
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
T' a = ContinuousLinearMap.id ℝ α
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s k1: HasFDerivWithinAt id (ContinuousLinearMap.id ℝ α) s a h2: HasFDerivWithinAt (f_inv ∘ f) (T' a) s a
T' a = ContinuousLinearMap.id ℝ α
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
T' a = ContinuousLinearMap.id ℝ α
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s k1: HasFDerivWithinAt id (ContinuousLinearMap.id ℝ α) s a h2: HasFDerivWithinAt (f_inv ∘ f) (T' a) s a
T' a = ContinuousLinearMap.id ℝ α
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s k1: HasFDerivWithinAt id (ContinuousLinearMap.id ℝ α) s a h2: HasFDerivWithinAt id (T' a) s a
T' a = ContinuousLinearMap.id ℝ α
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s k1: HasFDerivWithinAt id (ContinuousLinearMap.id ℝ α) s a h2: HasFDerivWithinAt id (T' a) s a
T' a = ContinuousLinearMap.id ℝ α
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s k1: HasFDerivWithinAt id (ContinuousLinearMap.id ℝ α) s a h2: HasFDerivWithinAt id (T' a) s a
T' a = ContinuousLinearMap.id ℝ α
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
T' a = ContinuousLinearMap.id ℝ α
Goals accomplished!
Goals accomplished!🐙
Goals accomplished!
Goals accomplished!🐙
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s
∀ a ∈ s, (T' a).det =1
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s key: T' a = ContinuousLinearMap.id ℝ α
(T' a).det =1
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s key: T' a = ContinuousLinearMap.id ℝ α
(ContinuousLinearMap.id ℝ α).det =1
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s key: T' a = ContinuousLinearMap.id ℝ α
(ContinuousLinearMap.id ℝ α).det =1
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s
∀ a ∈ s, (T' a).det =1
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s key: T' a = ContinuousLinearMap.id ℝ α
LinearMap.det ↑(ContinuousLinearMap.id ℝ α) =1
Goals accomplished!
α: Type u_1 β: Type u_2 inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α s: Set α T': α → α →L[ℝ] α f: α → β f_inv: β → α h1: is_reciprocal f f_inv h2: ∀ x ∈ s, HasFDerivWithinAt (f_inv ∘ f) (T' x) s x s_unique_diff: UniqueDiffOn ℝ s
∀ a ∈ s, (T' a).det =1
Goals accomplished!
Goals accomplished!🐙
end DetDerivative
namespace PushforwardDensity
variable {α : Type*} [MeasureSpace α] [NormedAddCommGroup α] [NormedSpace ℝ α]
(T' : α → α →L[ℝ] α) (μ : DensityMeasure α) (μ_t : Pushforward_Measure α α)
(h_μ : μ_t.μ = μ.toMeasure)
/-- Given a map T and a measure μ, if μ admits a density dμ w.r.t. the Lebesgue measure, then T#µ admits a density d x ↦ |det(∂ₓT x)| ⬝ dμ (T⁻¹ x)).-/
Goals accomplished!
Goals accomplished!
Goals accomplished!🐙
Goals accomplished!
α: Type u_1 inst✝⁵: MeasureSpace α inst✝⁴: NormedAddCommGroup α inst✝³: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure inst✝²: FiniteDimensional ℝ α inst✝¹: BorelSpace α inst✝: volume.IsAddHaarMeasure h1: ∀ (s : Set α), MeasurableSet s hT': ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x
∀ (s : Set α), μ_t.p_μ s =∫⁻ (x : α) in s, push_forward_density μ μ_t h_μ T' x
Goals accomplished!
α: Type u_1 inst✝⁵: MeasureSpace α inst✝⁴: NormedAddCommGroup α inst✝³: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure inst✝²: FiniteDimensional ℝ α inst✝¹: BorelSpace α inst✝: volume.IsAddHaarMeasure h1: ∀ (s : Set α), MeasurableSet s hT': ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x A: Set α
μ_t.p_μ A =∫⁻ (x : α) in A, push_forward_density μ μ_t h_μ T' x
-- We use pushforward measure and density definitions.
Goals accomplished!
α: Type u_1 inst✝⁵: MeasureSpace α inst✝⁴: NormedAddCommGroup α inst✝³: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure inst✝²: FiniteDimensional ℝ α inst✝¹: BorelSpace α inst✝: volume.IsAddHaarMeasure h1: ∀ (s : Set α), MeasurableSet s hT': ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x A: Set α
μ_t.p_μ A =∫⁻ (x : α) in A, push_forward_density μ μ_t h_μ T' x
Goals accomplished!
α: Type u_1 inst✝⁵: MeasureSpace α inst✝⁴: NormedAddCommGroup α inst✝³: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure inst✝²: FiniteDimensional ℝ α inst✝¹: BorelSpace α inst✝: volume.IsAddHaarMeasure h1: ∀ (s : Set α), MeasurableSet s hT': ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x A: Set α
μ_t.μ (μ_t.T_inv '' A) =∫⁻ (x : α) in A, push_forward_density μ μ_t h_μ T' x
Goals accomplished!
α: Type u_1 inst✝⁵: MeasureSpace α inst✝⁴: NormedAddCommGroup α inst✝³: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure inst✝²: FiniteDimensional ℝ α inst✝¹: BorelSpace α inst✝: volume.IsAddHaarMeasure h1: ∀ (s : Set α), MeasurableSet s hT': ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x A: Set α
μ_t.p_μ A =∫⁻ (x : α) in A, push_forward_density μ μ_t h_μ T' x
Goals accomplished!
α: Type u_1 inst✝⁵: MeasureSpace α inst✝⁴: NormedAddCommGroup α inst✝³: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure inst✝²: FiniteDimensional ℝ α inst✝¹: BorelSpace α inst✝: volume.IsAddHaarMeasure h1: ∀ (s : Set α), MeasurableSet s hT': ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x A: Set α
μ.toMeasure (μ_t.T_inv '' A) =∫⁻ (x : α) in A, push_forward_density μ μ_t h_μ T' x
Goals accomplished!
α: Type u_1 inst✝⁵: MeasureSpace α inst✝⁴: NormedAddCommGroup α inst✝³: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure inst✝²: FiniteDimensional ℝ α inst✝¹: BorelSpace α inst✝: volume.IsAddHaarMeasure h1: ∀ (s : Set α), MeasurableSet s hT': ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x A: Set α
μ.toMeasure (μ_t.T_inv '' A) =∫⁻ (x : α) in A, push_forward_density μ μ_t h_μ T' x
Goals accomplished!
α: Type u_1 inst✝⁵: MeasureSpace α inst✝⁴: NormedAddCommGroup α inst✝³: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure inst✝²: FiniteDimensional ℝ α inst✝¹: BorelSpace α inst✝: volume.IsAddHaarMeasure h1: ∀ (s : Set α), MeasurableSet s hT': ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x
∀ (s : Set α), μ_t.p_μ s =∫⁻ (x : α) in s, push_forward_density μ μ_t h_μ T' x
Goals accomplished!
α: Type u_1 inst✝⁵: MeasureSpace α inst✝⁴: NormedAddCommGroup α inst✝³: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure inst✝²: FiniteDimensional ℝ α inst✝¹: BorelSpace α inst✝: volume.IsAddHaarMeasure h1: ∀ (s : Set α), MeasurableSet s hT': ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x A: Set α
μ.toMeasure (μ_t.T_inv '' A) =∫⁻ (x : α) in A, push_forward_density μ μ_t h_μ T' x
Goals accomplished!
α: Type u_1 inst✝⁵: MeasureSpace α inst✝⁴: NormedAddCommGroup α inst✝³: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure inst✝²: FiniteDimensional ℝ α inst✝¹: BorelSpace α inst✝: volume.IsAddHaarMeasure h1: ∀ (s : Set α), MeasurableSet s hT': ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x A: Set α
∫⁻ (x : α) in μ_t.T_inv '' A, μ.d x =∫⁻ (x : α) in A, push_forward_density μ μ_t h_μ T' x
Goals accomplished!
α: Type u_1 inst✝⁵: MeasureSpace α inst✝⁴: NormedAddCommGroup α inst✝³: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure inst✝²: FiniteDimensional ℝ α inst✝¹: BorelSpace α inst✝: volume.IsAddHaarMeasure h1: ∀ (s : Set α), MeasurableSet s hT': ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x A: Set α
∫⁻ (x : α) in μ_t.T_inv '' A, μ.d x =∫⁻ (x : α) in A, push_forward_density μ μ_t h_μ T' x
-- We show that f_inv is injective on A using the fact that f is bijective.
Goals accomplished!
α: Type u_1 inst✝⁵: MeasureSpace α inst✝⁴: NormedAddCommGroup α inst✝³: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure inst✝²: FiniteDimensional ℝ α inst✝¹: BorelSpace α inst✝: volume.IsAddHaarMeasure h1: ∀ (s : Set α), MeasurableSet s hT': ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x A: Set α
∫⁻ (x : α) in μ_t.T_inv '' A, μ.d x =∫⁻ (x : α) in A, push_forward_density μ μ_t h_μ T' x
Goals accomplished!
Goals accomplished!🐙
Goals accomplished!
α: Type u_1 inst✝⁵: MeasureSpace α inst✝⁴: NormedAddCommGroup α inst✝³: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure inst✝²: FiniteDimensional ℝ α inst✝¹: BorelSpace α inst✝: volume.IsAddHaarMeasure h1: ∀ (s : Set α), MeasurableSet s hT': ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x A: Set α
Set.InjOn μ_t.T_inv A
Goals accomplished!
α: Type u_1 inst✝⁵: MeasureSpace α inst✝⁴: NormedAddCommGroup α inst✝³: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure inst✝²: FiniteDimensional ℝ α inst✝¹: BorelSpace α inst✝: volume.IsAddHaarMeasure h1: ∀ (s : Set α), MeasurableSet s hT': ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x A: Set α
Set.InjOn μ_t.T_inv A
Goals accomplished!
α: Type u_1 inst✝⁵: MeasureSpace α inst✝⁴: NormedAddCommGroup α inst✝³: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure inst✝²: FiniteDimensional ℝ α inst✝¹: BorelSpace α inst✝: volume.IsAddHaarMeasure h1: ∀ (s : Set α), MeasurableSet s hT': ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x A: Set α
Set.InjOn μ_t.T_inv A
Goals accomplished!
α: Type u_1 inst✝⁵: MeasureSpace α inst✝⁴: NormedAddCommGroup α inst✝³: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure inst✝²: FiniteDimensional ℝ α inst✝¹: BorelSpace α inst✝: volume.IsAddHaarMeasure h1: ∀ (s : Set α), MeasurableSet s hT': ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x A: Set α
a
is_injective μ_t.T_inv
Goals accomplished!
α: Type u_1 inst✝⁵: MeasureSpace α inst✝⁴: NormedAddCommGroup α inst✝³: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure inst✝²: FiniteDimensional ℝ α inst✝¹: BorelSpace α inst✝: volume.IsAddHaarMeasure h1: ∀ (s : Set α), MeasurableSet s hT': ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x A: Set α
Set.InjOn μ_t.T_inv A
Goals accomplished!
α: Type u_1 inst✝⁵: MeasureSpace α inst✝⁴: NormedAddCommGroup α inst✝³: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure inst✝²: FiniteDimensional ℝ α inst✝¹: BorelSpace α inst✝: volume.IsAddHaarMeasure h1: ∀ (s : Set α), MeasurableSet s hT': ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x A: Set α key: is_bijective μ_t.T_inv
a
is_injective μ_t.T_inv
Goals accomplished!
α: Type u_1 inst✝⁵: MeasureSpace α inst✝⁴: NormedAddCommGroup α inst✝³: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure inst✝²: FiniteDimensional ℝ α inst✝¹: BorelSpace α inst✝: volume.IsAddHaarMeasure h1: ∀ (s : Set α), MeasurableSet s hT': ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x A: Set α
Set.InjOn μ_t.T_inv A
Goals accomplished!
Goals accomplished!🐙
Goals accomplished!
Goals accomplished!🐙
-- Change of variable in integration.
Goals accomplished!
α: Type u_1 inst✝⁵: MeasureSpace α inst✝⁴: NormedAddCommGroup α inst✝³: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure inst✝²: FiniteDimensional ℝ α inst✝¹: BorelSpace α inst✝: volume.IsAddHaarMeasure h1: ∀ (s : Set α), MeasurableSet s hT': ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x A: Set α T_invisInjonA: Set.InjOn μ_t.T_inv A
∫⁻ (x : α) in μ_t.T_inv '' A, μ.d x =∫⁻ (x : α) in A, push_forward_density μ μ_t h_μ T' x
Goals accomplished!
α: Type u_1 inst✝⁵: MeasureSpace α inst✝⁴: NormedAddCommGroup α inst✝³: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure inst✝²: FiniteDimensional ℝ α inst✝¹: BorelSpace α inst✝: volume.IsAddHaarMeasure h1: ∀ (s : Set α), MeasurableSet s hT': ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x A: Set α T_invisInjonA: Set.InjOn μ_t.T_inv A
∫⁻ (x : α) in A, ENNReal.ofReal |(T' x).det|* μ.d (μ_t.T_inv x) =∫⁻ (x : α) in A, push_forward_density μ μ_t h_μ T' x
Goals accomplished!
α: Type u_1 inst✝⁵: MeasureSpace α inst✝⁴: NormedAddCommGroup α inst✝³: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure inst✝²: FiniteDimensional ℝ α inst✝¹: BorelSpace α inst✝: volume.IsAddHaarMeasure h1: ∀ (s : Set α), MeasurableSet s hT': ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x A: Set α T_invisInjonA: Set.InjOn μ_t.T_inv A
∫⁻ (x : α) in A, ENNReal.ofReal |(T' x).det|* μ.d (μ_t.T_inv x) =∫⁻ (x : α) in A, push_forward_density μ μ_t h_μ T' x
Goals accomplished!
α: Type u_1 inst✝⁵: MeasureSpace α inst✝⁴: NormedAddCommGroup α inst✝³: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure inst✝²: FiniteDimensional ℝ α inst✝¹: BorelSpace α inst✝: volume.IsAddHaarMeasure h1: ∀ (s : Set α), MeasurableSet s hT': ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x
∀ (s : Set α), μ_t.p_μ s =∫⁻ (x : α) in s, push_forward_density μ μ_t h_μ T' x
Goals accomplished!
α: Type u_1 inst✝⁵: MeasureSpace α inst✝⁴: NormedAddCommGroup α inst✝³: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure inst✝²: FiniteDimensional ℝ α inst✝¹: BorelSpace α inst✝: volume.IsAddHaarMeasure h1: ∀ (s : Set α), MeasurableSet s hT': ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x A: Set α T_invisInjonA: Set.InjOn μ_t.T_inv A
∫⁻ (x : α) in A, ENNReal.ofReal |(T' x).det|* μ.d (μ_t.T_inv x) =∫⁻ (x : α) in A, ENNReal.ofReal |(T' x).det|* μ.d (μ_t.T_inv x)
Goals accomplished!
α: Type u_1 inst✝⁵: MeasureSpace α inst✝⁴: NormedAddCommGroup α inst✝³: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure inst✝²: FiniteDimensional ℝ α inst✝¹: BorelSpace α inst✝: volume.IsAddHaarMeasure h1: ∀ (s : Set α), MeasurableSet s hT': ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x
∀ (s : Set α), μ_t.p_μ s =∫⁻ (x : α) in s, push_forward_density μ μ_t h_μ T' x
Goals accomplished!
Goals accomplished!🐙
variable {s : Set α}
/--When composing the density of a pushforward measure with a function, the composition appears **inside** the derivative.-/def push_forward_density_composition (f : α → α) (T_compose' : α → α →L[ℝ] α)
(_h1 : ∀ x ∈ s, HasFDerivWithinAt (μ_t.T_inv ∘ f) (T_compose' x) s x) :=
∀ (x : α), (push_forward_density μ μ_t h_μ T' ∘ f) x
= ENNReal.ofReal |(T_compose' x).det|* μ.d ((μ_t.T_inv ∘ f) x)
/--Given a map T and a measure μ such that it admits a density dμ w.r.t. the Lebesgue measure, then the composition between the density of T#μ d and T equals dμ : d ∘ T = dμ-/
Goals accomplished!
Goals accomplished!
Goals accomplished!🐙
Goals accomplished!
α: Type u_1 inst✝²: MeasureSpace α inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure s: Set α T_compose': α → α →L[ℝ] α h: ∀ x ∈ s, HasFDerivWithinAt (μ_t.T_inv ∘ μ_t.T) (T_compose' x) s x h2: push_forward_density_composition T' μ μ_t h_μ μ_t.T T_compose' h s_unique_diff: UniqueDiffOn ℝ s
∀ a ∈ s, (push_forward_density μ μ_t h_μ T' ∘ μ_t.T) a = μ.d a
Goals accomplished!
α: Type u_1 inst✝²: MeasureSpace α inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure s: Set α T_compose': α → α →L[ℝ] α h: ∀ x ∈ s, HasFDerivWithinAt (μ_t.T_inv ∘ μ_t.T) (T_compose' x) s x h2: push_forward_density_composition T' μ μ_t h_μ μ_t.T T_compose' h s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
(push_forward_density μ μ_t h_μ T' ∘ μ_t.T) a = μ.d a
Goals accomplished!
α: Type u_1 inst✝²: MeasureSpace α inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure s: Set α T_compose': α → α →L[ℝ] α h: ∀ x ∈ s, HasFDerivWithinAt (μ_t.T_inv ∘ μ_t.T) (T_compose' x) s x h2: push_forward_density_composition T' μ μ_t h_μ μ_t.T T_compose' h s_unique_diff: UniqueDiffOn ℝ s
∀ a ∈ s, (push_forward_density μ μ_t h_μ T' ∘ μ_t.T) a = μ.d a
Goals accomplished!
α: Type u_1 inst✝²: MeasureSpace α inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure s: Set α T_compose': α → α →L[ℝ] α h: ∀ x ∈ s, HasFDerivWithinAt (μ_t.T_inv ∘ μ_t.T) (T_compose' x) s x h2: push_forward_density_composition T' μ μ_t h_μ μ_t.T T_compose' h s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
(push_forward_density μ μ_t h_μ T' ∘ μ_t.T) a = μ.d a
Goals accomplished!
α: Type u_1 inst✝²: MeasureSpace α inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure s: Set α T_compose': α → α →L[ℝ] α h: ∀ x ∈ s, HasFDerivWithinAt (μ_t.T_inv ∘ μ_t.T) (T_compose' x) s x h2: push_forward_density_composition T' μ μ_t h_μ μ_t.T T_compose' h s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
ENNReal.ofReal |(T_compose' a).det|* μ.d ((μ_t.T_inv ∘ μ_t.T) a) = μ.d a
Goals accomplished!
α: Type u_1 inst✝²: MeasureSpace α inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure s: Set α T_compose': α → α →L[ℝ] α h: ∀ x ∈ s, HasFDerivWithinAt (μ_t.T_inv ∘ μ_t.T) (T_compose' x) s x h2: push_forward_density_composition T' μ μ_t h_μ μ_t.T T_compose' h s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
ENNReal.ofReal |(T_compose' a).det|* μ.d ((μ_t.T_inv ∘ μ_t.T) a) = μ.d a
Goals accomplished!
α: Type u_1 inst✝²: MeasureSpace α inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure s: Set α T_compose': α → α →L[ℝ] α h: ∀ x ∈ s, HasFDerivWithinAt (μ_t.T_inv ∘ μ_t.T) (T_compose' x) s x h2: push_forward_density_composition T' μ μ_t h_μ μ_t.T T_compose' h s_unique_diff: UniqueDiffOn ℝ s
∀ a ∈ s, (push_forward_density μ μ_t h_μ T' ∘ μ_t.T) a = μ.d a
Goals accomplished!
α: Type u_1 inst✝²: MeasureSpace α inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure s: Set α T_compose': α → α →L[ℝ] α h: ∀ x ∈ s, HasFDerivWithinAt (μ_t.T_inv ∘ μ_t.T) (T_compose' x) s x h2: push_forward_density_composition T' μ μ_t h_μ μ_t.T T_compose' h s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
ENNReal.ofReal |(T_compose' a).det|* μ.d ((μ_t.T_inv ∘ μ_t.T) a) = μ.d a
Goals accomplished!
α: Type u_1 inst✝²: MeasureSpace α inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure s: Set α T_compose': α → α →L[ℝ] α h: ∀ x ∈ s, HasFDerivWithinAt (μ_t.T_inv ∘ μ_t.T) (T_compose' x) s x h2: push_forward_density_composition T' μ μ_t h_μ μ_t.T T_compose' h s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
ENNReal.ofReal |(T_compose' a).det|* μ.d (id a) = μ.d a
Goals accomplished!
α: Type u_1 inst✝²: MeasureSpace α inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure s: Set α T_compose': α → α →L[ℝ] α h: ∀ x ∈ s, HasFDerivWithinAt (μ_t.T_inv ∘ μ_t.T) (T_compose' x) s x h2: push_forward_density_composition T' μ μ_t h_μ μ_t.T T_compose' h s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
ENNReal.ofReal |(T_compose' a).det|* μ.d (id a) = μ.d a
Goals accomplished!
α: Type u_1 inst✝²: MeasureSpace α inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure s: Set α T_compose': α → α →L[ℝ] α h: ∀ x ∈ s, HasFDerivWithinAt (μ_t.T_inv ∘ μ_t.T) (T_compose' x) s x h2: push_forward_density_composition T' μ μ_t h_μ μ_t.T T_compose' h s_unique_diff: UniqueDiffOn ℝ s
∀ a ∈ s, (push_forward_density μ μ_t h_μ T' ∘ μ_t.T) a = μ.d a
Goals accomplished!
α: Type u_1 inst✝²: MeasureSpace α inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure s: Set α T_compose': α → α →L[ℝ] α h: ∀ x ∈ s, HasFDerivWithinAt (μ_t.T_inv ∘ μ_t.T) (T_compose' x) s x h2: push_forward_density_composition T' μ μ_t h_μ μ_t.T T_compose' h s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
ENNReal.ofReal |(T_compose' a).det|* μ.d (id a) = μ.d a
Goals accomplished!
α: Type u_1 inst✝²: MeasureSpace α inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure s: Set α T_compose': α → α →L[ℝ] α h: ∀ x ∈ s, HasFDerivWithinAt (μ_t.T_inv ∘ μ_t.T) (T_compose' x) s x h2: push_forward_density_composition T' μ μ_t h_μ μ_t.T T_compose' h s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
ENNReal.ofReal |1|* μ.d (id a) = μ.d a
Goals accomplished!
α: Type u_1 inst✝²: MeasureSpace α inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure s: Set α T_compose': α → α →L[ℝ] α h: ∀ x ∈ s, HasFDerivWithinAt (μ_t.T_inv ∘ μ_t.T) (T_compose' x) s x h2: push_forward_density_composition T' μ μ_t h_μ μ_t.T T_compose' h s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
ENNReal.ofReal |(T_compose' a).det|* μ.d (id a) = μ.d a
Goals accomplished!
α: Type u_1 inst✝²: MeasureSpace α inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure s: Set α T_compose': α → α →L[ℝ] α h: ∀ x ∈ s, HasFDerivWithinAt (μ_t.T_inv ∘ μ_t.T) (T_compose' x) s x h2: push_forward_density_composition T' μ μ_t h_μ μ_t.T T_compose' h s_unique_diff: UniqueDiffOn ℝ s a: α ainS: a ∈ s
ENNReal.ofReal |1|* μ.d (id a) = μ.d a
Goals accomplished!
α: Type u_1 inst✝²: MeasureSpace α inst✝¹: NormedAddCommGroup α inst✝: NormedSpace ℝ α T': α → α →L[ℝ] α μ: DensityMeasure α μ_t: Pushforward_Measure α α h_μ: μ_t.μ = μ.toMeasure s: Set α T_compose': α → α →L[ℝ] α h: ∀ x ∈ s, HasFDerivWithinAt (μ_t.T_inv ∘ μ_t.T) (T_compose' x) s x h2: push_forward_density_composition T' μ μ_t h_μ μ_t.T T_compose' h s_unique_diff: UniqueDiffOn ℝ s
∀ a ∈ s, (push_forward_density μ μ_t h_μ T' ∘ μ_t.T) a = μ.d a
Goals accomplished!
Goals accomplished!🐙
end PushforwardDensity
variable {α β : Type*} [MeasureSpace α] [MeasureSpace β] [NormedAddCommGroup α] [NormedSpace ℝ α]
variable (μ_t : Pushforward_Measure α α) (μ : DensityMeasure α) (h_μ : μ_t.μ = μ.toMeasure)
[IsProbabilityMeasure μ_t.μ] [IsProbabilityMeasure μ_t.p_μ]
variable (T' : α → α →L[ℝ] α) (hT' : ∀ (s : Set α), ∀ x ∈ s, HasFDerivWithinAt μ_t.T_inv (T' x) s x)
variable (π : DensityMeasure α) (π_t : Pushforward_Measure α α) (h_π : π_t.μ = π.toMeasure)
variable (Tπ' : α → α →L[ℝ] α)
open PushforwardDensity
/-- **Main resutlt:** Given a map T and two measures μ π, both admitting density w.r.t. the Lebesgue measure, then KL(T#μ || π) = KL(μ || T⁻¹#π).-/
Goals accomplished!
Goals accomplished!
Goals accomplished!🐙
-- We use the composition propriety of the pushforward measure