LeanMachineLearning exposition

MeasureTheory.StronglyMeasurable.div₀'🔗

Minimal Lean file

div₀'🔗

LemmaMeasureTheory.StronglyMeasurable.div₀'
Details

No docstring.

🔗theorem
MeasureTheory.StronglyMeasurable.div₀'.{u_4, u_5} {𝓐 : Type u_4}
  {β : Type u_5} {m𝓐 : MeasurableSpace 𝓐} [TopologicalSpace β]
  [GroupWithZero β] [ContinuousMul β] [ContinuousInv₀ β]
  [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β]
  [BorelSpace β] [MeasurableSingletonClass β] {f g : 𝓐 → β}
  (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) :
  StronglyMeasurable (f / g)
MeasureTheory.StronglyMeasurable.div₀'.{u_4,
    u_5}
  {𝓐 : Type u_4} {β : Type u_5}
  {m𝓐 : MeasurableSpace 𝓐}
  [TopologicalSpace β] [GroupWithZero β]
  [ContinuousMul β] [ContinuousInv₀ β]
  [TopologicalSpace.PseudoMetrizableSpace
      β]
  [MeasurableSpace β] [BorelSpace β]
  [MeasurableSingletonClass β]
  {f g : 𝓐 → β}
  (hf : StronglyMeasurable f)
  (hg : StronglyMeasurable g) :
  StronglyMeasurable (f / g)

Code

lemma _root_.MeasureTheory.StronglyMeasurable.div₀' {𝓐 β : Type*}
    {m𝓐 : MeasurableSpace 𝓐} [TopologicalSpace β]
    [GroupWithZero β] [ContinuousMul β] [ContinuousInv₀ β]
    [TopologicalSpace.PseudoMetrizableSpace β]
    [MeasurableSpace β] [BorelSpace β] [MeasurableSingletonClass β]
    {f g : 𝓐 → β} (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) :
    StronglyMeasurable (f / g)
Used by (1)

Actions: Source · Open Issue

Proof
by
  refine ⟨fun n => hf.approx n / (hg.approx n).restrict {x | g x ≠ 0}, fun x => ?_⟩
  have : MeasurableSet {x | g x ≠ 0} := ((MeasurableSet.singleton 0).preimage hg.measurable).compl
  by_cases h : g x = 0
  · simp_all only [ne_eq, SimpleFunc.coe_div, SimpleFunc.coe_restrict, Pi.div_apply, mem_setOf_eq,
      not_true_eq_false, not_false_eq_true, indicator_of_notMem, _root_.div_zero]
    exact tendsto_const_nhds
  · simp_all only [ne_eq, SimpleFunc.coe_div, SimpleFunc.coe_restrict,
      Pi.div_apply, mem_setOf_eq, not_false_eq_true, indicator_of_mem]
    exact (hf.tendsto_approx x).div (hg.tendsto_approx x) h