OAI/Analysis/ProductSpaces/WeakNullity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.IndependentProducts.weaklyNull_of_orthogonal_fixed_norm line 17
  2. def OAI.IndependentProducts.l2ToL1 line 49

    Source documentation

    The canonical continuous inclusion L2 -> L1 on a probability space.

    def l2ToL1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 1 ν :=
…
  3. lemma OAI.IndependentProducts.l2ToL1_coe line 58
  4. lemma OAI.IndependentProducts.norm_l2ToL1_le line 60
  5. def OAI.IndependentProducts.childIncrementL2 line 72

    Source documentation

    The child jump in the Hilbert space L2.

    def childIncrementL2 (v : Vertex) (n : ℕ) : Lp ℝ 2 (productMeasure μ) :=
…

    Mentions: OAI.IndependentProducts.Vertex, OAI.IndependentProducts.productMeasure

  6. lemma OAI.IndependentProducts.childIncrementL2_ae line 76
  7. lemma OAI.IndependentProducts.l2ToL1_childIncrement line 89
  8. lemma OAI.IndependentProducts.childIncrementL2_norm_constant line 101
  9. lemma OAI.IndependentProducts.indepFun_pathSquare_mul_child line 121
  10. lemma OAI.IndependentProducts.childIncrementL2_orthogonal line 150
  11. lemma OAI.IndependentProducts.weaklyNull_child_difference line 178
  12. theorem OAI.IndependentProducts.main_general line 203

    Source documentation

    The closed L1 product span is infinite dimensional and admits no equivalent AUC norm.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasureTheory.Measure, Real, OAI.IndependentProducts.MultiplierHypotheses, And, Not, FiniteDimensional, Subtype, MeasureTheory.AEEqFun, OAI.IndependentProducts.Sample, OAI.IndependentProducts.Edge, OAI.IndependentProducts.productMeasure, Membership.mem, AddSubgroup, MeasureTheory.Lp, OfNat.ofNat, ENNReal, Submodule, OAI.IndependentProducts.productSpan, Seminorm, OAI.IndependentProducts.IsEquivalentNorm and 1 more

    Proof uses: MeasureTheory.IsProbabilityMeasure, OAI.IndependentProducts.MultiplierHypotheses.probability, OAI.IndependentProducts.Vertex, OAI.IndependentProducts.WeaklyNull, Nat, HSub.hSub, OAI.IndependentProducts.pathVector, OAI.IndependentProducts.MultiplierHypotheses.second_moment, OAI.IndependentProducts.child, OAI.IndependentProducts.weaklyNull_child_difference, OAI.IndependentProducts.MultiplierHypotheses.positive, OAI.IndependentProducts.MultiplierHypotheses.mean_one, OAI.IndependentProducts.MultiplierHypotheses.nonconstant, Eq, Norm.norm, MeasureTheory.integral, abs, OAI.IndependentProducts.norm_child_difference, LT.lt, OAI.IndependentProducts.mean_abs_deviation_pos and 6 more

    171 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: ComparatorChallenges/IndependentProducts.lean:89 (same statement text; different proof or body). Qualify references as OAI.IndependentProducts.main_general@path.

    Tactic trace: 9 steps

    Open to load the checked before-and-after goal states.

    theorem main_general (μ : Measure ℝ) (hμ : MultiplierHypotheses μ) :
    ¬ FiniteDimensional ℝ (productSpan μ) ∧
    ∀ N : Seminorm ℝ (productSpan μ),
      IsEquivalentNorm (productSpan μ) N → ¬ IsAUC (productSpan μ) N := by
…

    Mentions: OAI.IndependentProducts.productSpan, OAI.IndependentProducts.IsEquivalentNorm, OAI.IndependentProducts.IsAUC