Source indexedlemma · leanprover/lean4:v4.33.0-rc1

condMultiDist_of_cast

PFR.BoundingMutual · PFR/BoundingMutual.lean:77 to 94

Mathematical statement

Exact Lean statement

lemma condMultiDist_of_cast {m m' : ℕ} (h : m' = m) {Ω : Fin m → Type*}
    (hΩ : ∀ i, MeasureSpace (Ω i))
    {G S : Type*} [MeasurableFinGroup G] [Fintype S] (X : ∀ i, Ω i → G) (Y : ∀ i, Ω i → S) :
    D[fun i ↦ X (i.cast h) | fun i ↦ Y (i.cast h); fun i ↦ hΩ (i.cast h)] =
    D[X | Y ; hΩ]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma condMultiDist_of_cast {m m' : ℕ} (h : m' = m) {Ω : Fin m → Type*}    (hΩ : ∀ i, MeasureSpace (Ω i))    {G S : Type*} [MeasurableFinGroup G] [Fintype S] (X : ∀ i, Ω i → G) (Y : ∀ i, Ω i → S) :    D[fun i ↦ X (i.cast h) | fun i ↦ Y (i.cast h); fun i ↦ hΩ (i.cast h)] =    D[X | Y ; hΩ] := by  unfold condMultiDist  let ι : (Fin m' → S) → (Fin m → S) := fun x i ↦ x (i.cast h.symm)  have hι : Function.Bijective ι := by    constructor    · intro f g h'; ext i; replace h' := congrFun h' (i.cast h); simpa [ι] using h'    intro f; use f ∘ (Fin.cast h); ext i; simp [ι]  convert Function.Bijective.sum_comp hι _ with y _  congr 1  · convert Function.Bijective.prod_comp (Fin.cast_bijective h) _ with i _    rfl  convert multiDist_of_cast h _ _ X with i hmes i  · simp; congr  intros; simp; infer_instance