`Learning.IsAlgEnvSeq.memLp_means_action`🔗

Lemma

No docstring.

theorem

Learning.IsAlgEnvSeq.memLp_means_action.{u_1, u_2, u_3} {Ω : Type u_1}
  {𝓐 : Type u_2} {𝓨 : Type u_3} {mΩ : MeasurableSpace Ω}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {A : ℕ → Ω → 𝓐}
  {Y : ℕ → Ω → 𝓨} {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure P] {alg : Algorithm 𝓐 𝓨}
  {env : Environment 𝓐 𝓨} [SecondCountableTopology 𝓨] [BorelSpace 𝓨]
  (h : IsAlgEnvSeq A Y alg env P) {n : ℕ} {p : ENNReal} (hp1 : 1 ≤ p)
  (hp_top : p ≠ ⊤) (hint : MeasureTheory.MemLp (Y n) p P) :
  MeasureTheory.MemLp (fun ω => Environment.means env A Y (A n ω) n ω) p
    P
Learning.IsAlgEnvSeq.memLp_means_action.{u_1,
    u_2, u_3}
  {Ω : Type u_1} {𝓐 : Type u_2}
  {𝓨 : Type u_3} {mΩ : MeasurableSpace Ω}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨]
  {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure P]
  {alg : Algorithm 𝓐 𝓨}
  {env : Environment 𝓐 𝓨}
  [SecondCountableTopology 𝓨]
  [BorelSpace 𝓨]
  (h : IsAlgEnvSeq A Y alg env P) {n : ℕ}
  {p : ENNReal} (hp1 : 1 ≤ p)
  (hp_top : p ≠ ⊤)
  (hint : MeasureTheory.MemLp (Y n) p P) :
  MeasureTheory.MemLp
    (fun ω =>
      Environment.means env A Y (A n ω) n
        ω)
    p P

Code

lemma IsAlgEnvSeq.memLp_means_action [SecondCountableTopology 𝓨] [BorelSpace 𝓨]
    (h : IsAlgEnvSeq A Y alg env P) {n : ℕ} {p : ℝ≥0∞} (hp1 : 1 ≤ p) (hp_top : p ≠ ∞)
    (hint : MemLp (Y n) p P) :
    MemLp (fun ω ↦ env.means A Y (A n ω) n ω) p P

Proof

by
  have hp0 : p ≠ 0 := by positivity
  have hA := h.measurable_action
  have h_hist := h.measurable_history
  have hint' : MemLp id p (P.map (Y n)) := by
    rwa [memLp_map_measure_iff (by fun_prop) (h.measurable_feedback _).aemeasurable]
  unfold Environment.means Environment.measure
  cases n with
  | zero =>
    simp only [↓reduceIte, id_eq]
    rw [h.hasLaw_feedback_zero_comp.map_eq, Measure.memLp_comp_iff hp0 hp_top (by fun_prop)]
      at hint'
    have hint'' := hint'.2.comp_aemeasurable (by fun_prop)
    have h_eq ω : env.ν0 (A 0 ω) = (env.ν0 ∘ₖ Kernel.deterministic (A 0) (by fun_prop)) ω := by
      simp [Kernel.comp_deterministic_eq_comap]
    rw [← integrable_norm_rpow_iff _ hp0 hp_top]
    swap
    · refine StronglyMeasurable.aestronglyMeasurable ?_
      simp_rw [h_eq]
      exact StronglyMeasurable.integral_kernel (by fun_prop)
    simp only [id_eq] at hint''
    refine Integrable.mono' hint'' ?_ ?_
    · refine ((AEMeasurable.norm ?_).pow_const _).aestronglyMeasurable
      refine (StronglyMeasurable.measurable ?_).aemeasurable
      simp_rw [h_eq]
      exact StronglyMeasurable.integral_kernel (by fun_prop)
    · simp only [Real.norm_eq_abs, Function.comp_apply]
      filter_upwards [ae_of_ae_map (hA 0).aemeasurable hint'.1] with ω hω
      rw [abs_of_nonneg (by positivity)]
      exact norm_integral_rpow_le_integral_norm_rpow hp1 hp_top hω
  | succ n =>
    simp only [Nat.add_eq_zero_iff, one_ne_zero, and_false, ↓reduceIte, Nat.add_one_sub_one, id_eq]
    rw [(h.hasLaw_feedback_comp n).map_eq, Measure.memLp_comp_iff hp0 hp_top (by fun_prop)] at hint'
    have hint'' := hint'.2.comp_aemeasurable (by fun_prop)
    have h_eq ω : (env.feedback n) (history A Y n ω, A (n + 1) ω) =
        (env.feedback n ∘ₖ
          Kernel.deterministic (fun ω ↦ (history A Y n ω, A (n + 1) ω)) (by fun_prop)) ω := by
      simp [Kernel.comp_deterministic_eq_comap]
    rw [← integrable_norm_rpow_iff _ hp0 hp_top]
    swap
    · refine StronglyMeasurable.aestronglyMeasurable ?_
      simp_rw [Kernel.sectR_apply, h_eq]
      exact StronglyMeasurable.integral_kernel (by fun_prop)
    simp only [id_eq] at hint''
    refine Integrable.mono' hint'' ?_ ?_
    · refine ((AEMeasurable.norm ?_).pow_const _).aestronglyMeasurable
      refine (StronglyMeasurable.measurable ?_).aemeasurable
      simp_rw [Kernel.sectR_apply, h_eq]
      exact StronglyMeasurable.integral_kernel (by fun_prop)
    · simp only [Real.norm_eq_abs, Function.comp_apply, Kernel.sectR_apply]
      filter_upwards [ae_of_ae_map ((h_hist n).prodMk (hA (n + 1))).aemeasurable hint'.1]
        with ω hω
      rw [abs_of_nonneg (by positivity)]
      exact norm_integral_rpow_le_integral_norm_rpow hp1 hp_top hω

Actions: Source · Open Issue

New in v4.34.0-rc2-14-gf86702d (2026-08-25), and its meaning has not changed since.

Self-contained, with its dependencies inlined and proofs replaced by sorry: download the raw file · open it in the Lean web editor.

Dependency graph

Audit surface: 6 project declarations, 73 external constants

✓ Proved: no sorry anywhere in its closure

This is the tool's own reading of one build's recorded axioms, and it is not robust against an author who wants it to pass. Checking meant to be relied on should go through Comparator, which replays the proof through the kernel from an export against an explicit list of permitted axioms.

Learning.IsAlgEnvSeq.memLp_means_action🔗

`Learning.IsAlgEnvSeq.memLp_means_action`🔗