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

multiTau_continuous

PFR.MultiTauFunctional · PFR/MultiTauFunctional.lean:96 to 118

Source documentation

If $G$ is finite, then $\tau$ is continuous.

Exact Lean statement

lemma multiTau_continuous {G Ω₀ : Type u} [MeasurableFinGroup G] [TopologicalSpace G]
    [DiscreteTopology G] [BorelSpace G] [MeasureSpace Ω₀] (p : multiRefPackage G Ω₀) :
    Continuous (fun (μ : Fin p.m → ProbabilityMeasure G) ↦
      multiTau p (fun _ ↦ G) (fun i ↦ ⟨μ i⟩) (fun _ ↦ id))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma multiTau_continuous {G Ω₀ : Type u} [MeasurableFinGroup G] [TopologicalSpace G]    [DiscreteTopology G] [BorelSpace G] [MeasureSpace Ω₀] (p : multiRefPackage G Ω₀) :    Continuous (fun (μ : Fin p.m → ProbabilityMeasure G) ↦      multiTau p (fun _ ↦ G) (fun i ↦ ⟨μ i⟩) (fun _ ↦ id)) := by  simp only [multiTau, multiDist, Measure.map_id]  apply Continuous.add (Continuous.sub ?_ ?_) ?_  · let f : (Fin p.m → G) → G := fun x ↦ ∑ i, x i    have fcont : Continuous f := by fun_prop    change Continuous fun (x : Fin p.m → ProbabilityMeasure G) ↦      Hm[(ProbabilityMeasure.map (ProbabilityMeasure.pi x) fcont.aemeasurable : Measure G)]    apply continuous_measureEntropy_probabilityMeasure.comp    exact (ProbabilityMeasure.continuous_map fcont).comp ProbabilityMeasure.continuous_pi  · apply Continuous.mul continuous_const    refine continuous_finsetSum Finset.univ ?_    intro i hi    apply continuous_entropy_restrict_probabilityMeasure.comp    exact continuous_apply i  · apply Continuous.mul continuous_const    refine continuous_finsetSum Finset.univ ?_    intro i hi    have := p.hprob    apply (continuous_rdist_restrict_probabilityMeasure₁_left p.X₀ volume p.hmeas).comp    exact continuous_apply i