LeanPool.RlTheoryInLean.Defs

theorem Tendsto.filter_congr {α : Type u_1} {β : Type u_2} {f : α → β} {a : Filter α} {b b' : Filter β} (hb : b = b') (hf : Filter.Tendsto f a b) : Filter.Tendsto f a b'

theorem Kernel.congrFun_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {κ₁ κ₂ : ProbabilityTheory.Kernel α β} (h : κ₁ = κ₂) (a : α) : κ₁ a = κ₂ a

theorem Measurable.congr {α : Type u_1} {β : Type u_2} {ma : MeasurableSpace α} {mb : MeasurableSpace β} {f g : α → β} (hfg : f = g) : Measurable f → Measurable g

theorem Integrable.measure_congr {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {β : Type u_2} {f : α → β} [NormedAddCommGroup β] [NormedSpace ℝ β] {hμν : μ = ν} (hf : MeasureTheory.Integrable f μ) : MeasureTheory.Integrable f ν

theorem Integral.measure_congr {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {β : Type u_2} {f : α → β} [NormedAddCommGroup β] [NormedSpace ℝ β] {hμν : μ = ν} : ∫ (x : α), f x ∂μ = ∫ (x : α), f x ∂ν

theorem HasDerivAt.congr {f g : ℝ → ℝ} {f' x : ℝ} (hfg : f = g) (h : HasDerivAt f f' x) : HasDerivAt g f' x

theorem HasDerivAt.congr_congr {f g : ℝ → ℝ} {f' g' x : ℝ} (h : HasDerivAt f f' x) (hfg : f = g) (hfg' : f' = g') : HasDerivAt g g' x

@[reducible, inline]

abbrev RLTheory.E (d : ℕ) : Type

Euclidean space of dimension d, used for finite-dimensional RL iterates.

Equations

• RLTheory.E d = EuclideanSpace ℝ (Fin d)