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

continuous_tau_restrict_probabilityMeasure

PFR.TauFunctional · PFR/TauFunctional.lean:79 to 92

Mathematical statement

Exact Lean statement

lemma continuous_tau_restrict_probabilityMeasure
    [TopologicalSpace G] [DiscreteTopology G] [BorelSpace G] :
    Continuous
      (fun (μ : ProbabilityMeasure G × ProbabilityMeasure G) ↦ τ[id ; μ.1 # id ; μ.2 | p])

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma continuous_tau_restrict_probabilityMeasure    [TopologicalSpace G] [DiscreteTopology G] [BorelSpace G] :    Continuous      (fun (μ : ProbabilityMeasure G × ProbabilityMeasure G) ↦ τ[id ; μ.1 # id ; μ.2 | p]) := by  have obs₁ : Continuous      (fun (μ : ProbabilityMeasure G × ProbabilityMeasure G) ↦ d[p.X₀₂ ; ℙ # id ; μ.2]) :=    Continuous.comp (continuous_rdist_restrict_probabilityMeasure₁' _ _ p.hmeas2) continuous_snd  have obs₂ : Continuous      (fun (μ : ProbabilityMeasure G × ProbabilityMeasure G) ↦ d[id ; μ.1.toMeasure # id ; μ.2]) :=    continuous_rdist_restrict_probabilityMeasure  have obs₃ : Continuous      (fun (μ : ProbabilityMeasure G × ProbabilityMeasure G) ↦ d[p.X₀₁ ; ℙ # id ; μ.1]) :=    Continuous.comp (continuous_rdist_restrict_probabilityMeasure₁' _ _ p.hmeas1) continuous_fst  continuity