Commit 2023-06-21 09:25 63c43dd9

View on Github →

feat: port Counterexamples.Phillips (#5282)

Estimated changes

Modified Counterexamples.lean

Created Counterexamples/Phillips.lean

added def ContinuousLinearMap.toBoundedAdditiveMeasure

added def Counterexample.DiscreteCopy

added def Counterexample.Phillips1940.BoundedAdditiveMeasure.C

added theorem Counterexample.Phillips1940.BoundedAdditiveMeasure.abs_le_bound

added theorem Counterexample.Phillips1940.BoundedAdditiveMeasure.additive

added theorem Counterexample.Phillips1940.BoundedAdditiveMeasure.apply_countable

added def Counterexample.Phillips1940.BoundedAdditiveMeasure.continuousPart

added theorem Counterexample.Phillips1940.BoundedAdditiveMeasure.continuousPart_apply_diff

added theorem Counterexample.Phillips1940.BoundedAdditiveMeasure.continuousPart_apply_eq_zero_of_countable

added theorem Counterexample.Phillips1940.BoundedAdditiveMeasure.countable_discreteSupport

added def Counterexample.Phillips1940.BoundedAdditiveMeasure.discretePart

added theorem Counterexample.Phillips1940.BoundedAdditiveMeasure.discretePart_apply

added def Counterexample.Phillips1940.BoundedAdditiveMeasure.discreteSupport

added theorem Counterexample.Phillips1940.BoundedAdditiveMeasure.empty

added theorem Counterexample.Phillips1940.BoundedAdditiveMeasure.eq_add_parts

added theorem Counterexample.Phillips1940.BoundedAdditiveMeasure.exists_discrete_support

added theorem Counterexample.Phillips1940.BoundedAdditiveMeasure.exists_discrete_support_nonpos

added theorem Counterexample.Phillips1940.BoundedAdditiveMeasure.le_bound

added theorem Counterexample.Phillips1940.BoundedAdditiveMeasure.neg_apply

added def Counterexample.Phillips1940.BoundedAdditiveMeasure.restrict

added theorem Counterexample.Phillips1940.BoundedAdditiveMeasure.restrict_apply

added structure Counterexample.Phillips1940.BoundedAdditiveMeasure

added theorem Counterexample.Phillips1940.apply_f_eq_continuousPart

added def Counterexample.Phillips1940.boundedIntegrableFunctions

added def Counterexample.Phillips1940.boundedIntegrableFunctionsIntegralCLM

added theorem Counterexample.Phillips1940.comp_ae_eq_const

added theorem Counterexample.Phillips1940.continuousPart_evalClm_eq_zero

added theorem Counterexample.Phillips1940.countable_compl_spf

added theorem Counterexample.Phillips1940.countable_ne

added theorem Counterexample.Phillips1940.countable_spf_mem

added theorem Counterexample.Phillips1940.exists_linear_extension_to_boundedFunctions

added theorem Counterexample.Phillips1940.extensionToBoundedFunctions_apply

added def Counterexample.Phillips1940.f

added theorem Counterexample.Phillips1940.integrable_comp

added theorem Counterexample.Phillips1940.integral_comp

added theorem Counterexample.Phillips1940.measurable_comp

added theorem Counterexample.Phillips1940.no_pettis_integral

added theorem Counterexample.Phillips1940.norm_bound

added theorem Counterexample.Phillips1940.norm_indicator_le_one

added theorem Counterexample.Phillips1940.sierpinski_pathological_family

added def Counterexample.Phillips1940.spf

added theorem Counterexample.Phillips1940.toFunctions_toMeasure

added theorem Counterexample.Phillips1940.toFunctions_toMeasure_continuousPart

added def MeasureTheory.Measure.extensionToBoundedFunctions